diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 771f09e81a582ee0566004b81d176a74ca506305..2c0ca4725b598602c937ac43e765e017b918f6ee 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -95,7 +95,7 @@ Ltac parse s :=
   | string => lazymatch eval vm_compute in (parse s) with
               | Some ?pats => pats | _ => fail "spec_pat.parse: cannot parse" s
               end
-  | ident => constr:([SIdent s])
+  | ident => constr:([SIdent s []])
   | ?X => fail "spec_pat.parse:" s "has unexpected type" X
   end.
 End spec_pat.