Commit bd2926f5 authored by Ralf Jung's avatar Ralf Jung
Browse files

remove Coq 8.10 compat code

parent dda0bf71
...@@ -154,21 +154,21 @@ Tactic failure: iInv: invariant "H2" not found. ...@@ -154,21 +154,21 @@ Tactic failure: iInv: invariant "H2" not found.
PROP : bi PROP : bi
============================ ============================
forall (P : PROP) (_ : True), bi_entails P P forall P (_ : True), bi_entails P P
"p2" "p2"
: string : string
1 subgoal 1 subgoal
PROP : bi PROP : bi
============================ ============================
forall P : PROP, and True (bi_entails P P) forall P, and True (bi_entails P P)
"p3" "p3"
: string : string
1 subgoal 1 subgoal
PROP : bi PROP : bi
============================ ============================
ex (fun P : PROP => bi_entails P P) ex (fun P => bi_entails P P)
"p4" "p4"
: string : string
1 subgoal 1 subgoal
......
...@@ -5,7 +5,6 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva ...@@ -5,7 +5,6 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva
From iris.bi Require Import ascii. From iris.bi Require Import ascii.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
Section base_logic_tests. Section base_logic_tests.
Context {M : ucmraT}. Context {M : ucmraT}.
......
...@@ -29,17 +29,17 @@ ...@@ -29,17 +29,17 @@
Objective0 : Objective Q Objective0 : Objective Q
𝓟, 𝓠 : PROP 𝓟, 𝓠 : PROP
============================ ============================
"H2" : ∀ i : I, Q i "H2" : ∀ i, Q i
"H3" : 𝓟 "H3" : 𝓟
"H4" : 𝓠 "H4" : 𝓠
--------------------------------------∗ --------------------------------------∗
∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i ∀ i, 𝓟 ∗ 𝓠 ∗ Q i
1 subgoal 1 subgoal
I : biIndex I : biIndex
PROP : bi PROP : bi
FU0 : BiFUpd PROP * () FU : BiFUpd PROP
P, Q : monPred P, Q : monPred
i : I i : I
============================ ============================
...@@ -50,7 +50,7 @@ ...@@ -50,7 +50,7 @@
I : biIndex I : biIndex
PROP : bi PROP : bi
FU0 : BiFUpd PROP * () FU : BiFUpd PROP
P : monPred P : monPred
i : I i : I
============================ ============================
......
From iris.proofmode Require Import tactics monpred. From iris.proofmode Require Import tactics monpred.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
Section tests. Section tests.
Context {I : biIndex} {PROP : bi}. Context {I : biIndex} {PROP : bi}.
...@@ -102,11 +101,7 @@ Section tests. ...@@ -102,11 +101,7 @@ Section tests.
iAssumption. iAssumption.
Qed. Qed.
(* This is a hack to avoid avoid coq bug #5735: sections variables ignore hint Context (FU : BiFUpd PROP).
modes. So we assume the instances in a way that cannot be used by type
class resolution, and then separately declare the instance as such. *)
Context (FU0 : BiFUpd PROP * unit).
Instance FU : BiFUpd PROP := fst FU0.
Lemma test_apply_fupd_intro_mask E1 E2 P : Lemma test_apply_fupd_intro_mask E1 E2 P :
E2 E1 P - |={E1,E2}=> |={E2,E1}=> P. E2 E1 P - |={E1,E2}=> |={E2,E1}=> P.
......
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