Commit 7cf966c4 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make iIntoEntails work when the entails is hidden under a delta.

parent f83ae863
...@@ -221,10 +221,12 @@ The tactic instantiates each dependent argument [x_i] with an evar and generates ...@@ -221,10 +221,12 @@ The tactic instantiates each dependent argument [x_i] with an evar and generates
a goal [P] for non-dependent arguments [x_i : P]. *) a goal [P] for non-dependent arguments [x_i : P]. *)
Tactic Notation "iIntoEntails" open_constr(t) := Tactic Notation "iIntoEntails" open_constr(t) :=
let rec go t := let rec go t :=
lazymatch type of t with let tT := type of t in
lazymatch eval hnf in tT with
| True _ => apply t | True _ => apply t
| _ _ => apply (uPred.entails_wand _ _ t) | _ _ => apply (uPred.entails_wand _ _ t)
| _ ⊣⊢ _ => apply (uPred.equiv_iff _ _ t) (* need to use the unfolded version of [⊣⊢] due to the hnf *)
| uPred_equiv' _ _ => apply (uPred.equiv_iff _ _ t)
| ?P ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H] | ?P ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
| _ : ?T, _ => | _ : ?T, _ =>
(* Put [T] inside an [id] to avoid TC inference from being invoked. *) (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
......
Supports Markdown
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