Commit 789b377b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix namespaces after previous rename.

parent 9a4dfca0
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
# This file is distributed under the terms of the BSD license. # This file is distributed under the terms of the BSD license.
import os, glob, string import os, glob, string
modules = ["prelude", "iris"] modules = ["prelude", "modures", "iris"]
Rs = '-Q . ""' Rs = '-Q . ""'
env = DefaultEnvironment(ENV = os.environ,tools=['default', 'Coq'], COQFLAGS=Rs) env = DefaultEnvironment(ENV = os.environ,tools=['default', 'Coq'], COQFLAGS=Rs)
......
Require Export iris.cmra. Require Export modures.cmra.
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
Record agree A `{Dist A} := Agree { Record agree A `{Dist A} := Agree {
......
Require Export iris.excl. Require Export modures.excl.
Local Arguments valid _ _ !_ /. Local Arguments valid _ _ !_ /.
Local Arguments validN _ _ _ !_ /. Local Arguments validN _ _ _ !_ /.
......
Require Export iris.ra iris.cofe. Require Export modures.ra modures.cofe.
Class ValidN (A : Type) := validN : nat A Prop. Class ValidN (A : Type) := validN : nat A Prop.
Instance: Params (@validN) 3. Instance: Params (@validN) 3.
......
Require Export iris.cmra iris.cofe_maps. Require Export modures.cmra modures.cofe_maps.
Require Import prelude.pmap prelude.natmap prelude.gmap. Require Import prelude.pmap prelude.natmap prelude.gmap.
(** option *) (** option *)
......
Require Export iris.cofe prelude.fin_maps. Require Export modures.cofe prelude.fin_maps.
Require Import prelude.pmap prelude.gmap prelude.natmap. Require Import prelude.pmap prelude.gmap prelude.natmap.
Local Obligation Tactic := idtac. Local Obligation Tactic := idtac.
......
Require Export iris.cofe. Require Export modures.cofe.
Section solver. Section solver.
Context (F : cofeT cofeT cofeT). Context (F : cofeT cofeT cofeT).
......
Require Export iris.ra iris.cmra. Require Export modures.ra modures.cmra.
(** From disjoint pcm *) (** From disjoint pcm *)
Record validity {A} (P : A Prop) : Type := Validity { Record validity {A} (P : A Prop) : Type := Validity {
......
Require Export iris.cmra. Require Export modures.cmra.
Local Arguments validN _ _ _ !_ /. Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /. Local Arguments valid _ _ !_ /.
......
Require Import iris.cmra. Require Import modures.cmra.
Local Hint Extern 1 (_ _) => etransitivity; [eassumption|]. Local Hint Extern 1 (_ _) => etransitivity; [eassumption|].
Local Hint Extern 1 (_ _) => etransitivity; [|eassumption]. Local Hint Extern 1 (_ _) => etransitivity; [|eassumption].
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
......
Require Export iris.ra. Require Export modures.ra.
Require Import prelude.sets iris.dra. Require Import prelude.sets modures.dra.
Local Arguments valid _ _ !_ /. Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /. Local Arguments op _ _ !_ !_ /.
Local Arguments unit _ _ !_ /. Local Arguments unit _ _ !_ /.
......
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