Commit c5e7fc1a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix error reporting of iSpecialize.

parent e8fb0e28
...@@ -381,7 +381,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) := ...@@ -381,7 +381,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
Local Tactic Notation "iSpecializePat" constr(H) constr(pat) := Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
let solve_to_wand H1 := let solve_to_wand H1 :=
apply _ || apply _ ||
let P := match goal with |- IntoWand ?P _ _ => P end in let P := match goal with |- IntoWand _ ?P _ _ => P end in
fail "iSpecialize:" P "not an implication/wand" in fail "iSpecialize:" P "not an implication/wand" in
let rec go H1 pats := let rec go H1 pats :=
lazymatch pats with lazymatch pats with
...@@ -394,8 +394,8 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) := ...@@ -394,8 +394,8 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
[env_reflexivity || fail "iSpecialize:" H2 "not found" [env_reflexivity || fail "iSpecialize:" H2 "not found"
|env_reflexivity || fail "iSpecialize:" H1 "not found" |env_reflexivity || fail "iSpecialize:" H1 "not found"
|apply _ || |apply _ ||
let P := match goal with |- IntoWand ?P ?Q _ => P end in let P := match goal with |- IntoWand _ ?P ?Q _ => P end in
let Q := match goal with |- IntoWand ?P ?Q _ => Q end in let Q := match goal with |- IntoWand _ ?P ?Q _ => Q end in
fail "iSpecialize: cannot instantiate" P "with" Q fail "iSpecialize: cannot instantiate" P "with" Q
|env_reflexivity|go H1 pats] |env_reflexivity|go H1 pats]
| SPureGoal ?d :: ?pats => | SPureGoal ?d :: ?pats =>
......
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