Commit ace0db94 authored by Ralf Jung's avatar Ralf Jung

Mostly revert the previous commit

It leads to wild unification errors on 8.11.  None of this makes any sense, but I guess that is expected with Coq...
parent 5726c91c
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 stdpp Require Import tactics.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Export invariants gen_heap.
From iris_examples.logrel.F_mu_ref_conc Require Export rules_binary typing.
From iris.program_logic Require Import weakestpre.
From iris.base_logic Require Import invariants.
From iris.algebra Require Import list.
From stdpp Require Import tactics.
From iris_examples.logrel.F_mu_ref_conc Require Export rules_binary typing.
Import uPred.
(* HACK: move somewhere else *)
......
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 Import invariants gen_heap.
From iris.program_logic Require Import weakestpre.
From iris.program_logic Require Import ectx_lifting.
From iris.base_logic Require Export gen_heap.
From iris_examples.logrel.F_mu_ref_conc Require Export lang.
Import uPred.
......
From iris.algebra Require Import excl auth frac agree gmap list.
From iris.proofmode Require Import tactics.
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 Export 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 gen_heap.
From iris_examples.logrel.F_mu_ref_conc Require Export fundamental_unary.
From iris.base_logic Require Import auth.
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