Commit 23ad2f43 authored by Robbert's avatar Robbert

Merge branch 'robbert/from_forall_tc_opaque' into 'master'

Missing `tc_opaque` instance for `FromForall`.

See merge request !357
parents 352c5d42 2c980e72
......@@ -109,6 +109,10 @@ Lemma test_very_fast_iIntros P :
x y : nat, ( x = y P - P)%I.
Proof. by iIntros. Qed.
Definition tc_opaque_test : PROP := tc_opaque ( x : nat, x = x )%I.
Lemma test_iIntros_tc_opaque : tc_opaque_test.
Proof. by iIntros (x). Qed.
(** Prior to 0b84351c this used to loop, now `iAssumption` instantiates `R` with
`False` and performs false elimination. *)
Lemma test_iAssumption_evar_ex_false : R, R P, P.
......
......@@ -619,6 +619,8 @@ Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
FromExist P Φ FromExist (tc_opaque P) Φ := id.
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) :
IntoExist P Φ IntoExist (tc_opaque P) Φ := id.
Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) :
FromForall P Φ FromForall (tc_opaque P) Φ := id.
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) :
IntoForall P Φ IntoForall (tc_opaque P) Φ := id.
Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}
......
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