Improve error messages for sel/spec/intro pat.

iris/proofmode/intro_patterns.v

@@ -136,23 +136,32 @@ Ltac parse s :=
   | intro_pat => constr:([s])
   | list string =>
      lazymatch eval vm_compute in (mjoin <$> mapM parse s) with
-     | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
+     | Some ?pats => pats
+     | _ => fail "intro_pat.parse: cannot parse" s "as an introduction pattern"
      end
   | string =>
      lazymatch eval vm_compute in (parse s) with
-     | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
+     | Some ?pats => pats
+     | _ => fail "intro_pat.parse: cannot parse" s "as an introduction pattern"
      end
   | ident => constr:([IIdent s])
-  | ?X => fail "intro_pat.parse:" s "has unexpected type" X
+  | ?X => fail "intro_pat.parse: the term" s
+     "is expected to be an introduction pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 Ltac parse_one s :=
   lazymatch type of s with
   | intro_pat => s
   | string =>
      lazymatch eval vm_compute in (parse s) with
-     | Some [?pat] => pat | _ => fail "intro_pat.parse_one: cannot parse" s
+     | Some [?pat] => pat
+     | _ => fail "intro_pat.parse_one: cannot parse" s "as an introduction pattern"
      end
-  | ?X => fail "intro_pat.parse_one:" s "has unexpected type" X
+  | ?X => fail "intro_pat.parse_one: the term" s
+     "is expected to be an introduction pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 End intro_pat.
 
@@ -176,5 +185,8 @@ Ltac intro_pat_intuitionistic p :=
      eval cbv in (forallb intro_pat_intuitionistic pat)
   | ident => false
   | bool => p
-  | ?X => fail "intro_pat_intuitionistic:" p "has unexpected type" X
+  | ?X => fail "intro_pat_intuitionistic: the term" p
+     "is expected to be an introduction pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.

iris/proofmode/sel_patterns.v

@@ -37,8 +37,12 @@ Ltac parse s :=
   | list string => eval vm_compute in (SelIdent ∘ INamed <$> s)
   | string =>
      lazymatch eval vm_compute in (parse s) with
-     | Some ?pats => pats | _ => fail "invalid sel_pat" s
+     | Some ?pats => pats
+     | _ => fail "sel_pat.parse: cannot parse" s "as a selection pattern"
      end
-  | ?X => fail "sel_pat.parse:" s "has unexpected type" X
+  | ?X => fail "sel_pat.parse: the term" s
+     "is expected to be a selection pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 End sel_pat.

iris/proofmode/spec_patterns.v

@@ -92,10 +92,15 @@ 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 "spec_pat.parse: cannot parse" s
-              end
+  | string =>
+     lazymatch eval vm_compute in (parse s) with
+     | Some ?pats => pats
+     | _ => fail "spec_pat.parse: cannot parse" s "as a specialization pattern"
+     end
   | ident => constr:([SIdent s []])
-  | ?X => fail "spec_pat.parse:" s "has unexpected type" X
+  | ?X => fail "spec_pat.parse: the term" s
+     "is expected to be a specialization pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 End spec_pat.

tests/proofmode.ref

@@ -730,11 +730,15 @@ Use [iApply fupd_mask_intro] to introduce mask-changing update modalities".
 "iRevert_wrong_sel_pat"
      : string
 The command has indeed failed with message:
-Tactic failure: sel_pat.parse: n has unexpected type nat.
+Tactic failure: sel_pat.parse: the term n
+is expected to be a selection pattern (usually a string),
+but has unexpected type nat.
 "iInduction_wrong_sel_pat"
      : string
 The command has indeed failed with message:
-Tactic failure: sel_pat.parse: m has unexpected type nat.
+Tactic failure: sel_pat.parse: the term m
+is expected to be a selection pattern (usually a string),
+but has unexpected type nat.
 "test_pure_name"
      : string
 1 goal