Commit 90cbf2a0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Clear temporary hypotheses created by iIntoEntails.

parent a52c62d1
...@@ -224,7 +224,7 @@ Tactic Notation "iIntoEntails" open_constr(t) := ...@@ -224,7 +224,7 @@ Tactic Notation "iIntoEntails" open_constr(t) :=
| True _ => apply t | True _ => apply t
| _ _ => apply (uPred.entails_wand _ _ t) | _ _ => apply (uPred.entails_wand _ _ t)
| _ _ => apply (uPred.equiv_iff _ _ t) | _ _ => apply (uPred.equiv_iff _ _ t)
| ?P ?Q => let H := fresh in assert P as H; [|go uconstr:(t 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. *)
(* This is a workarround for Coq bug #4969. *) (* This is a workarround for Coq bug #4969. *)
......
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