diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 2332ebac5c6c4f4dbfcd11214b1db5db76af457a..a2f10edb1d7e016a73dfcef5055c7c6077331897 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -15,7 +15,7 @@ Record spec_goal := SpecGoal {
 Inductive spec_pat :=
   | SForall : spec_pat
   | SIdent : ident → spec_pat
-  | SPureGoal : bool → spec_pat
+  | SPureGoal (perform_done : bool) : spec_pat
   | SGoal : spec_goal → spec_pat
   | SAutoFrame : goal_kind → spec_pat.