Commit 89196687 authored by Ralf Jung's avatar Ralf Jung

fix the rest of the repo for Coq 8.11

parent ea928791
......@@ -3,6 +3,10 @@
for Sequential Programs.
*)
(* Definition of invariants and their rules (expressed using the fancy update
modality). *)
From iris.base_logic.lib Require Export invariants.
(* Contains definitions of the weakest precondition assertion, and its basic rules. *)
From iris.program_logic Require Export weakestpre.
......@@ -18,10 +22,6 @@ From iris.heap_lang Require Export notation lang.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode.
(* Definition of invariants and their rules (expressed using the fancy update
modality). *)
From iris.base_logic.lib Require Export invariants.
(* The following line makes Coq check that we do not use any admitted facts /
additional assumptions not in the statement of the theorems being proved. *)
......
From iris_examples.logrel.F_mu Require Export fundamental.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
From iris_examples.logrel.F_mu Require Export fundamental.
Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
( `{irisG F_mu_lang Σ}, [] e : τ)
......
......@@ -22,7 +22,7 @@ Section fundamental.
Notation D := (prodO valO valO -n> iPropO Σ).
Implicit Types e : expr.
Implicit Types Δ : listO D.
Hint Resolve to_of_val.
Local Hint Resolve to_of_val : core.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w)
constr(Hv) uconstr(Hp) :=
......
......@@ -2,9 +2,9 @@ From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From iris.base_logic Require Export invariants.
From iris.algebra Require Import auth frac agree gmap.
From iris_examples.logrel.F_mu_ref Require Export lang.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Export gen_heap.
From iris_examples.logrel.F_mu_ref Require Export lang.
Import uPred.
Class heapG Σ := HeapG {
......@@ -50,11 +50,11 @@ Section lang_rules.
inversion H; subst; clear H
end.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
Local Hint Constructors head_step : core.
Local Hint Resolve alloc_fresh : core.
Local Hint Resolve to_of_val : core.
(** Base axioms for core primitives of the language: Stateful reductions. *)
Lemma wp_alloc E e v:
......
From iris.program_logic Require Import lifting.
From iris.algebra Require Import excl auth frac agree gmap list.
From iris_examples.logrel.F_mu_ref Require Export rules.
From iris.program_logic Require Import lifting.
From iris.proofmode Require Import tactics.
From iris_examples.logrel.F_mu_ref Require Export rules.
Import uPred.
Definition specN := nroot .@ "spec".
......@@ -47,7 +47,7 @@ Section cfg.
Implicit Types e : expr.
Implicit Types v : val.
Local Hint Resolve to_of_val.
Local Hint Resolve to_of_val : core.
(** Conversion to tpools and back *)
Lemma step_insert_no_fork K e σ κ e' σ' :
......
From iris_examples.logrel.F_mu_ref Require Export fundamental.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
From iris.base_logic Require Import auth.
From iris.program_logic Require Import adequacy.
From iris_examples.logrel.F_mu_ref Require Export fundamental.
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ;
......
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth list.
From iris.program_logic Require Import adequacy.
From iris_examples.logrel.F_mu_ref_conc Require Export examples.lock.
From iris_examples.logrel.F_mu_ref_conc Require Import soundness_binary.
From iris.program_logic Require Import adequacy.
Definition CG_increment (x : expr) : expr :=
Lam (Store x.[ren (+ 1)] (BinOp Add (#n 1) (Load x.[ren (+ 1)]))).
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
From iris_examples.logrel.F_mu_ref_conc Require Import
soundness_binary rules rules_binary.
From iris.program_logic Require Import adequacy.
Definition fact : expr :=
Rec (If (BinOp Eq (Var 1) (#n 0))
......
From iris.proofmode Require Import tactics.
From iris_examples.logrel.F_mu_ref_conc Require Import logrel_binary.
From iris.algebra Require Import auth gmap agree.
From iris_examples.logrel.F_mu_ref_conc Require Import logrel_binary.
Import uPred.
From iris.algebra Require deprecated.
Import deprecated.dec_agree.
......
From iris.algebra Require Import list.
From iris_examples.logrel.F_mu_ref_conc Require Export logrel_binary.
From iris.proofmode Require Import tactics.
From iris_examples.logrel.F_mu_ref_conc Require Import rules_binary.
From iris.program_logic Require Export lifting.
From iris_examples.logrel.F_mu_ref_conc Require Export logrel_binary.
From iris_examples.logrel.F_mu_ref_conc Require Import rules_binary.
Section bin_log_def.
Context `{heapIG Σ, cfgSG Σ}.
......@@ -22,7 +22,7 @@ Section fundamental.
Notation D := (prodO valO valO -n> iPropO Σ).
Implicit Types e : expr.
Implicit Types Δ : listO D.
Hint Resolve to_of_val : core.
Local Hint Resolve to_of_val : core.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w)
constr(Hv) uconstr(Hp) :=
......
From iris.base_logic Require Import invariants.
From iris.program_logic Require Import lifting.
From iris.proofmode Require Import tactics.
From iris_examples.logrel.F_mu_ref_conc Require Export logrel_unary.
From iris_examples.logrel.F_mu_ref_conc Require Import rules.
From iris.base_logic Require Export invariants.
From iris.program_logic Require Export lifting.
From iris.proofmode Require Import tactics.
Definition log_typed `{heapIG Σ} (Γ : list type) (e : expr) (τ : type) := Δ vs,
env_Persistent Δ
......
......@@ -2,9 +2,9 @@ From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From iris.base_logic Require Export invariants.
From iris.algebra Require Import auth frac agree gmap.
From iris_examples.logrel.F_mu_ref_conc Require Export lang.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Export gen_heap.
From iris_examples.logrel.F_mu_ref_conc Require Export lang.
Import uPred.
(** The CMRA for the heap of the implementation. This is linked to the
......
From iris.algebra Require Import excl auth frac agree gmap list.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.program_logic Require Import lifting.
From iris.algebra Require Import excl auth frac agree gmap list.
From iris_examples.logrel.F_mu_ref_conc Require Export rules.
From iris.proofmode Require Import tactics.
Import uPred.
Definition specN := nroot .@ "spec".
......
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