Commit b5fcf2eb authored by Robbert Krebbers's avatar Robbert Krebbers

More consistent specialization patterns for iAssert.

parent c7bd7639
...@@ -694,14 +694,14 @@ Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4) ...@@ -694,14 +694,14 @@ Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
(** * Assert *) (** * Assert *)
Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) := Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
let H := iFresh in let H := iFresh in
let Hs := spec_pat.parse_one Hs in let Hs := spec_pat.parse Hs in
lazymatch Hs with lazymatch Hs with
| SAssert ?lr ?Hs => | [SAssert ?lr ?Hs] =>
eapply tac_assert with _ _ _ lr Hs H Q; (* (js:=Hs) (j:=H) (P:=Q) *) eapply tac_assert with _ _ _ lr Hs H Q; (* (js:=Hs) (j:=H) (P:=Q) *)
[env_cbv; reflexivity || fail "iAssert:" Hs "not found" [env_cbv; reflexivity || fail "iAssert:" Hs "not found"
|env_cbv; reflexivity| |env_cbv; reflexivity|
|iDestructHyp H as pat] |iDestructHyp H as pat]
| SPersistent => | [SAssert true [] :: SAlways] =>
eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *) eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
[apply _ || fail "iAssert:" Q "not persistent" [apply _ || fail "iAssert:" Q "not persistent"
|env_cbv; reflexivity| |env_cbv; reflexivity|
......
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