Commit 6a3c7402 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Error message when the deprecated * specialization pattern is used.

parent fdfc790d
...@@ -12,7 +12,8 @@ Inductive spec_pat := ...@@ -12,7 +12,8 @@ Inductive spec_pat :=
| SGoal : spec_goal spec_pat | SGoal : spec_goal spec_pat
| SGoalPersistent : spec_pat | SGoalPersistent : spec_pat
| SGoalPure : spec_pat | SGoalPure : spec_pat
| SName : string spec_pat. | SName : string spec_pat
| SForall : spec_pat.
Module spec_pat. Module spec_pat.
Inductive token := Inductive token :=
...@@ -22,6 +23,7 @@ Inductive token := ...@@ -22,6 +23,7 @@ Inductive token :=
| TBracketR : token | TBracketR : token
| TPersistent : token | TPersistent : token
| TPure : token | TPure : token
| TForall : token
| TModal : token | TModal : token
| TFrame : token. | TFrame : token.
...@@ -35,6 +37,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token := ...@@ -35,6 +37,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "]" s => tokenize_go s (TBracketR :: cons_name kn k) "" | String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
| String "#" s => tokenize_go s (TPersistent :: cons_name kn k) "" | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
| String "%" s => tokenize_go s (TPure :: cons_name kn k) "" | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
| String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
| String ">" s => tokenize_go s (TModal :: cons_name kn k) "" | String ">" s => tokenize_go s (TModal :: cons_name kn k) ""
| String "$" s => tokenize_go s (TFrame :: cons_name kn k) "" | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
| String a s => | String a s =>
...@@ -57,6 +60,7 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) ...@@ -57,6 +60,7 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
| TBracketL :: ts => parse_goal ts (SpecGoal false false [] []) k | TBracketL :: ts => parse_goal ts (SpecGoal false false [] []) k
| TModal :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k | TModal :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k
| TModal :: ts => parse_go ts (SGoal (SpecGoal true true [] []) :: k) | TModal :: ts => parse_go ts (SGoal (SpecGoal true true [] []) :: k)
| TForall :: ts => parse_go ts (SForall :: k)
| _ => None | _ => None
end end
with parse_goal (ts : list token) (g : spec_goal) with parse_goal (ts : list token) (g : spec_goal)
......
...@@ -285,6 +285,9 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) := ...@@ -285,6 +285,9 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
let rec go H1 pats := let rec go H1 pats :=
lazymatch pats with lazymatch pats with
| [] => idtac | [] => idtac
| SForall :: ?pats =>
idtac "the * specialization pattern is deprecated because it is applied implicitly";
go H1 pats
| SName ?H2 :: ?pats => | SName ?H2 :: ?pats =>
eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *) eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
[env_cbv; reflexivity || fail "iSpecialize:" H2 "not found" [env_cbv; reflexivity || fail "iSpecialize:" H2 "not found"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment