Commit 508a1c8c authored by Ralf Jung's avatar Ralf Jung
Browse files

move algebra.base -> prelude.prelude

parent 0d44837e
......@@ -15,6 +15,7 @@
-arg -w -arg -redundant-canonical-projection
iris/prelude/options.v
iris/prelude/prelude.v
iris/algebra/monoid.v
iris/algebra/cmra.v
iris/algebra/big_op.v
......@@ -25,7 +26,6 @@ iris/algebra/view.v
iris/algebra/auth.v
iris/algebra/gmap.v
iris/algebra/ofe.v
iris/algebra/base.v
iris/algebra/dra.v
iris/algebra/cofe_solver.v
iris/algebra/agree.v
......
From iris.algebra Require Export base.
From iris.prelude Require Export prelude.
From iris.prelude Require Import options.
Set Primitive Projections.
......
(** An axiomatization of evaluation-context based languages, including a proof
that this gives rise to a "language" in the Iris sense. *)
From iris.algebra Require Export base.
From iris.prelude Require Export prelude.
From iris.program_logic Require Import language.
From iris.prelude Require Import options.
......
(** An axiomatization of languages based on evaluation context items, including
a proof that these are instances of general ectx-based languages. *)
From iris.algebra Require Export base.
From iris.prelude Require Export prelude.
From iris.program_logic Require Import language ectx_language.
From iris.prelude Require Import options.
......
From Coq Require Export Ascii.
From stdpp Require Export strings.
From iris.algebra Require Export base.
From iris.prelude Require Export prelude.
From iris.prelude Require Import options.
(** * Utility definitions used by the proofmode *)
......
From iris.algebra Require Export base.
From iris.prelude Require Export prelude.
From iris.bi Require Export bi.
From iris.proofmode Require Import base.
From iris.prelude Require Import options.
......
From stdpp Require Import countable numbers gmap.
From iris.algebra Require Import base.
From iris.prelude Require Export prelude.
From iris.prelude Require Import options.
Record loc := { loc_car : Z }.
......
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