diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index cc8feb04a746f5b61ad54dca1d413536c283167c..e24ab1e675ecc8b65a1901c5c5dc5283fdb2a5b5 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -128,11 +128,11 @@ Ltac parse s :=
   | intro_pat => constr:([s])
   | list string =>
      lazymatch eval vm_compute in (mjoin <$> mapM parse s) with
-     | Some ?pats => pats | _ => fail "invalid list intro_pat" s
+     | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
      end
   | string =>
      lazymatch eval vm_compute in (parse s) with
-     | Some ?pats => pats | _ => fail "invalid list intro_pat" s
+     | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
      end
   | ident => constr:([IIdent s])
   | ?X => fail "intro_pat.parse:" s "has unexpected type" X
@@ -142,7 +142,7 @@ Ltac parse_one s :=
   | intro_pat => s
   | string =>
      lazymatch eval vm_compute in (parse s) with
-     | Some [?pat] => pat | _ => fail "invalid intro_pat" s
+     | Some [?pat] => pat | _ => fail "intro_pat.parse_one: cannot parse" s
      end
   | ?X => fail "intro_pat.parse_one:" s "has unexpected type" X
   end.
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 64201daf270d2f560a1a6356fe8682588c4e990a..dd93c0ebec00f8a7bd7e013c9cae889f83163a2d 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -72,8 +72,11 @@ Definition parse (s : string) : option (list spec_pat) :=
 Ltac parse s :=
   lazymatch type of s with
   | list spec_pat => s
+  | spec_pat => constr:([s])
   | string => lazymatch eval vm_compute in (parse s) with
-              | Some ?pats => pats | _ => fail "invalid list spec_pat" s
+              | Some ?pats => pats | _ => fail "spec_pat.parse: cannot parse" s
               end
+  | ident => constr:([SIdent s])
+  | ?X => fail "spec_pat.parse:" s "has unexpected type" X
   end.
 End spec_pat.