Commit 4ca6213e authored by Robbert Krebbers's avatar Robbert Krebbers

Omit hypothesis name from many proof mode errors.

In most cases it is a temporary whose name is useless and just
clutters the error message.
parent ade2edb9
Pipeline #2569 passed with stage
in 4 minutes and 16 seconds
...@@ -107,14 +107,14 @@ Local Tactic Notation "iPersistent" constr(H) := ...@@ -107,14 +107,14 @@ Local Tactic Notation "iPersistent" constr(H) :=
eapply tac_persistent with _ H _ _ _; (* (i:=H) *) eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
[env_cbv; reflexivity || fail "iPersistent:" H "not found" [env_cbv; reflexivity || fail "iPersistent:" H "not found"
|let Q := match goal with |- IntoPersistentP ?Q _ => Q end in |let Q := match goal with |- IntoPersistentP ?Q _ => Q end in
apply _ || fail "iPersistent:" H ":" Q "not persistent" apply _ || fail "iPersistent:" Q "not persistent"
|env_cbv; reflexivity|]. |env_cbv; reflexivity|].
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) := Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
eapply tac_pure with _ H _ _ _; (* (i:=H1) *) eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
[env_cbv; reflexivity || fail "iPure:" H "not found" [env_cbv; reflexivity || fail "iPure:" H "not found"
|let P := match goal with |- IntoPure ?P _ => P end in |let P := match goal with |- IntoPure ?P _ => P end in
apply _ || fail "iPure:" H ":" P "not pure" apply _ || fail "iPure:" P "not pure"
|intros pat]. |intros pat].
Tactic Notation "iPureIntro" := Tactic Notation "iPureIntro" :=
...@@ -139,14 +139,15 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) := ...@@ -139,14 +139,15 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
| _ => | _ =>
eapply tac_forall_specialize with _ H _ _ _ xs; (* (i:=H) (a:=x) *) eapply tac_forall_specialize with _ H _ _ _ xs; (* (i:=H) (a:=x) *)
[env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found" [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
|apply _ || fail 1 "iSpecialize:" H "not a forall of the right arity or type" |let P := match goal with |- ForallSpecialize _ ?P _ => P end in
apply _ || fail 1 "iSpecialize:" P "not a forall of the right arity or type"
|cbn [himpl hcurry]; reflexivity|] |cbn [himpl hcurry]; reflexivity|]
end. end.
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 :=
let P := match goal with |- IntoWand ?P _ _ => P end in let P := match goal with |- IntoWand ?P _ _ => P end in
apply _ || fail "iSpecialize:" H1 ":" P "not an implication/wand" in apply _ || fail "iSpecialize:" P "not an implication/wand" in
let rec go H1 pats := let rec go H1 pats :=
lazymatch pats with lazymatch pats with
| [] => idtac | [] => idtac
...@@ -157,7 +158,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) := ...@@ -157,7 +158,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
|env_cbv; reflexivity || fail "iSpecialize:" H1 "not found" |env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|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
apply _ || fail "iSpecialize: cannot instantiate" H1 ":" P "with" H2 ":" Q apply _ || fail "iSpecialize: cannot instantiate" P "with" Q
|env_cbv; reflexivity|go H1 pats] |env_cbv; reflexivity|go H1 pats]
| SName true ?H2 :: ?pats => | SName true ?H2 :: ?pats =>
eapply tac_specialize_persistent with _ _ H1 _ _ _ _; eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
...@@ -270,7 +271,7 @@ Tactic Notation "iApply" open_constr(lem) := ...@@ -270,7 +271,7 @@ Tactic Notation "iApply" open_constr(lem) :=
|eapply tac_apply with _ H _ _ _; |eapply tac_apply with _ H _ _ _;
[env_cbv; reflexivity || fail 1 "iApply:" H "not found" [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
|let P := match goal with |- IntoWand ?P _ _ => P end in |let P := match goal with |- IntoWand ?P _ _ => P end in
apply _ || fail 1 "iApply: cannot apply" H ":" P apply _ || fail 1 "iApply: cannot apply" P
|lazy beta (* reduce betas created by instantiation *)]] in |lazy beta (* reduce betas created by instantiation *)]] in
lazymatch lem with lazymatch lem with
| ITrm ?t ?xs ?pat => | ITrm ?t ?xs ?pat =>
...@@ -362,7 +363,7 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) := ...@@ -362,7 +363,7 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *) eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
[env_cbv; reflexivity || fail "iOrDestruct:" H "not found" [env_cbv; reflexivity || fail "iOrDestruct:" H "not found"
|let P := match goal with |- IntoOr ?P _ _ => P end in |let P := match goal with |- IntoOr ?P _ _ => P end in
apply _ || fail "iOrDestruct:" H ":" P "not a disjunction" apply _ || fail "iOrDestruct:" P "not a disjunction"
|env_cbv; reflexivity || fail "iOrDestruct:" H1 "not fresh" |env_cbv; reflexivity || fail "iOrDestruct:" H1 "not fresh"
|env_cbv; reflexivity || fail "iOrDestruct:" H2 "not fresh"| |]. |env_cbv; reflexivity || fail "iOrDestruct:" H2 "not fresh"| |].
...@@ -398,7 +399,7 @@ Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) := ...@@ -398,7 +399,7 @@ Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
eapply tac_sep_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *) eapply tac_sep_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
[env_cbv; reflexivity || fail "iSepDestruct:" H "not found" [env_cbv; reflexivity || fail "iSepDestruct:" H "not found"
|let P := match goal with |- IntoSep _ ?P _ _ => P end in |let P := match goal with |- IntoSep _ ?P _ _ => P end in
apply _ || fail "iSepDestruct:" H ":" P "not separating destructable" apply _ || fail "iSepDestruct:" P "not separating destructable"
|env_cbv; reflexivity || fail "iSepDestruct:" H1 "or" H2 " not fresh"|]. |env_cbv; reflexivity || fail "iSepDestruct:" H1 "or" H2 " not fresh"|].
Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) := Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
...@@ -407,7 +408,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) := ...@@ -407,7 +408,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
|env_cbv; reflexivity || fail "iCombine:" H2 "not found" |env_cbv; reflexivity || fail "iCombine:" H2 "not found"
|let P1 := match goal with |- FromSep _ ?P1 _ => P1 end in |let P1 := match goal with |- FromSep _ ?P1 _ => P1 end in
let P2 := match goal with |- FromSep _ _ ?P2 => P2 end in let P2 := match goal with |- FromSep _ _ ?P2 => P2 end in
apply _ || fail "iCombine: cannot combine" H1 ":" P1 "and" H2 ":" P2 apply _ || fail "iCombine: cannot combine" P1 "and" P2
|env_cbv; reflexivity || fail "iCombine:" H "not fresh"|]. |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
(** Framing *) (** Framing *)
...@@ -479,7 +480,7 @@ Local Tactic Notation "iExistDestruct" constr(H) ...@@ -479,7 +480,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *) eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
[env_cbv; reflexivity || fail "iExistDestruct:" H "not found" [env_cbv; reflexivity || fail "iExistDestruct:" H "not found"
|let P := match goal with |- IntoExist ?P _ => P end in |let P := match goal with |- IntoExist ?P _ => P end in
apply _ || fail "iExistDestruct:" H ":" P "not an existential"|]; apply _ || fail "iExistDestruct:" P "not an existential"|];
let y := fresh in let y := fresh in
intros y; eexists; split; intros y; eexists; split;
[env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh" [env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh"
...@@ -517,7 +518,7 @@ Tactic Notation "iVsCore" constr(H) := ...@@ -517,7 +518,7 @@ Tactic Notation "iVsCore" constr(H) :=
[env_cbv; reflexivity || fail "iVs:" H "not found" [env_cbv; reflexivity || fail "iVs:" H "not found"
|let P := match goal with |- ElimVs ?P _ _ _ => P end in |let P := match goal with |- ElimVs ?P _ _ _ => P end in
let Q := match goal with |- ElimVs _ _ ?Q _ => Q end in let Q := match goal with |- ElimVs _ _ ?Q _ => Q end in
apply _ || fail "iVs: cannot run" H ":" P "in" Q apply _ || fail "iVs: cannot run" P "in" Q
"because the goal or hypothesis is not a view shift" "because the goal or hypothesis is not a view shift"
|env_cbv; reflexivity|]. |env_cbv; reflexivity|].
...@@ -849,7 +850,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) := ...@@ -849,7 +850,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
eapply (tac_rewrite _ Heq _ _ lr); eapply (tac_rewrite _ Heq _ _ lr);
[env_cbv; reflexivity || fail "iRewrite:" Heq "not found" [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
|let P := match goal with |- ?P _ => P end in |let P := match goal with |- ?P _ => P end in
reflexivity || fail "iRewrite:" Heq ":" P "not an equality" reflexivity || fail "iRewrite:" P "not an equality"
|iRewriteFindPred |iRewriteFindPred
|intros ??? ->; reflexivity|lazy beta; iClear Heq]). |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
...@@ -862,7 +863,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) ...@@ -862,7 +863,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
[env_cbv; reflexivity || fail "iRewrite:" Heq "not found" [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
|env_cbv; reflexivity || fail "iRewrite:" H "not found" |env_cbv; reflexivity || fail "iRewrite:" H "not found"
|let P := match goal with |- ?P _ => P end in |let P := match goal with |- ?P _ => P end in
reflexivity || fail "iRewrite:" Heq ":" P "not an equality" reflexivity || fail "iRewrite:" P "not an equality"
|iRewriteFindPred |iRewriteFindPred
|intros ??? ->; reflexivity |intros ??? ->; reflexivity
|env_cbv; reflexivity|lazy beta; iClear Heq]). |env_cbv; reflexivity|lazy beta; iClear Heq]).
......
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