Commit 5726c91c authored by Ralf Jung's avatar Ralf Jung

fix more imports to hopefully work both on 8.10 and 8.11

parent 89196687
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import tactics.
From iris_examples.logrel.F_mu_ref_conc Require Export rules_binary typing.
......
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import invariants.
From iris_examples.logrel.F_mu_ref_conc Require Import examples.lock.
Import uPred.
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Export invariants.
From iris.base_logic Require Export invariants gen_heap.
From iris_examples.logrel.F_mu_ref_conc Require Export rules_binary typing.
From iris.algebra Require Import list.
From stdpp Require Import tactics.
......
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.proofmode Require Import tactics.
From iris.base_logic Require Export gen_heap.
From iris.base_logic Require Import invariants gen_heap.
From iris.program_logic Require Import weakestpre.
From iris.program_logic Require Import ectx_lifting.
From iris_examples.logrel.F_mu_ref_conc Require Export lang.
Import uPred.
......@@ -45,12 +44,12 @@ Section lang_rules.
inversion H; subst; clear H
end.
Local Hint Extern 0 (atomic _) => solve_atomic.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Extern 0 (atomic _) => solve_atomic : core.
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.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.base_logic Require Import invariants gen_heap.
From iris.program_logic Require Import language ectx_language ectxi_language.
From iris.program_logic Require Import lifting.
From iris_examples.logrel.F_mu_ref_conc Require Export rules.
Import uPred.
......
From iris_examples.logrel.F_mu_ref_conc Require Export fundamental_unary.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
From iris.base_logic Require Import auth.
From iris.base_logic Require Import gen_heap.
From iris_examples.logrel.F_mu_ref_conc Require Export fundamental_unary.
Class heapPreIG Σ := HeapPreIG {
heap_preG_iris :> invPreG Σ;
......
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