From dcff8ded2b64738c838a552487ae9e4d4630015b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 16 Nov 2015 11:38:22 +0100
Subject: [PATCH] Use qualified module names and coqc -Q instead of -R.
---
theories/assoc.v | 4 ++--
theories/collections.v | 2 +-
theories/countable.v | 2 +-
theories/decidable.v | 2 +-
theories/error.v | 2 +-
theories/fin_collections.v | 4 ++--
theories/fin_map_dom.v | 2 +-
theories/fin_maps.v | 2 +-
theories/finite.v | 2 +-
theories/hashset.v | 4 ++--
theories/lexico.v | 2 +-
theories/list.v | 2 +-
theories/listset.v | 2 +-
theories/listset_nodup.v | 2 +-
theories/mapset.v | 2 +-
theories/natmap.v | 2 +-
theories/nmap.v | 4 ++--
theories/numbers.v | 2 +-
theories/option.v | 2 +-
theories/optionmap.v | 4 ++--
theories/orders.v | 2 +-
theories/pmap.v | 4 ++--
theories/prelude.v | 26 +++++++++++++-------------
theories/pretty.v | 4 ++--
theories/proof_irrel.v | 2 +-
theories/relations.v | 2 +-
theories/sets.v | 4 ++--
theories/streams.v | 2 +-
theories/stringmap.v | 4 ++--
theories/tactics.v | 2 +-
theories/vector.v | 2 +-
theories/zmap.v | 4 ++--
32 files changed, 54 insertions(+), 54 deletions(-)
diff --git a/theories/assoc.v b/theories/assoc.v
index c9e609ba..3b8730a5 100644
--- a/theories/assoc.v
+++ b/theories/assoc.v
@@ -6,8 +6,8 @@ main advantage of these association lists compared to search trees, is that it
has canonical representatives and thus extensional Leibniz equality. Compared
to a naive unordered association list, the merge operation (used for unions,
intersections, and difference) is also linear-time. *)
-Require Import mapset.
-Require Export fin_maps.
+Require Import prelude.mapset.
+Require Export prelude.fin_maps.
(** Because the association list is sorted using [strict lexico] instead of
[lexico], it automatically guarantees that no duplicates exist. *)
diff --git a/theories/collections.v b/theories/collections.v
index eaff59e0..7caafe69 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -3,7 +3,7 @@
(** This file collects definitions and theorems on collections. Most
importantly, it implements some tactics to automatically solve goals involving
collections. *)
-Require Export base tactics orders.
+Require Export prelude.base prelude.tactics prelude.orders.
Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
∀ x, x ∈ X → x ∈ Y.
diff --git a/theories/countable.v b/theories/countable.v
index c62eb235..628aa552 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -1,6 +1,6 @@
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
-Require Export list.
+Require Export prelude.list.
Local Obligation Tactic := idtac.
Local Open Scope positive.
diff --git a/theories/decidable.v b/theories/decidable.v
index 96720b24..184372c8 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -3,7 +3,7 @@
(** This file collects theorems, definitions, tactics, related to propositions
with a decidable equality. Such propositions are collected by the [Decision]
type class. *)
-Require Export proof_irrel.
+Require Export prelude.proof_irrel.
Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.
diff --git a/theories/error.v b/theories/error.v
index 46fe0c57..0eb6c33f 100644
--- a/theories/error.v
+++ b/theories/error.v
@@ -1,6 +1,6 @@
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
-Require Export list.
+Require Export prelude.list.
Definition error (S E A : Type) : Type := S → E + (A * S).
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index f4e63f63..28591e60 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -3,8 +3,8 @@
(** This file collects definitions and theorems on finite collections. Most
importantly, it implements a fold and size function and some useful induction
principles on finite collections . *)
-Require Import Permutation relations listset.
-Require Export numbers collections.
+Require Import Permutation prelude.relations prelude.listset.
+Require Export prelude.numbers prelude.collections.
Instance collection_size `{Elements A C} : Size C := length ∘ elements.
Definition collection_fold `{Elements A C} {B}
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index bbdbb8ea..f69fabec 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -3,7 +3,7 @@
(** This file provides an axiomatization of the domain function of finite
maps. We provide such an axiomatization, instead of implementing the domain
function in a generic way, to allow more efficient implementations. *)
-Require Export collections fin_maps.
+Require Export prelude.collections prelude.fin_maps.
Class FinMapDom K M D `{FMap M,
∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index b77edcd4..7e12d0e4 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -5,7 +5,7 @@ finite maps and collects some theory on it. Most importantly, it proves useful
induction principles for finite maps and implements the tactic
[simplify_map_equality] to simplify goals involving finite maps. *)
Require Import Permutation.
-Require Export relations vector orders.
+Require Export prelude.relations prelude.vector prelude.orders.
(** * Axiomatization of finite maps *)
(** We require Leibniz equality to be extensional on finite maps. This of
diff --git a/theories/finite.v b/theories/finite.v
index 9aa8a459..78240011 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -1,6 +1,6 @@
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
-Require Export countable list.
+Require Export prelude.countable prelude.list.
Obligation Tactic := idtac.
Class Finite A `{∀ x y : A, Decision (x = y)} := {
diff --git a/theories/hashset.v b/theories/hashset.v
index 345ba837..f517f0e7 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -3,8 +3,8 @@
(** This file implements finite set using hash maps. Hash sets are represented
using radix-2 search trees. Each hash bucket is thus indexed using an binary
integer of type [Z], and contains an unordered list without duplicates. *)
-Require Export fin_maps listset.
-Require Import zmap.
+Require Export prelude.fin_maps prelude.listset.
+Require Import prelude.zmap.
Record hashset {A} (hash : A → Z) := Hashset {
hashset_car : Zmap (list A);
diff --git a/theories/lexico.v b/theories/lexico.v
index e36b552a..31ddc33b 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This files defines a lexicographic order on various common data structures
and proves that it is a partial order having a strong variant of trichotomy. *)
-Require Import numbers.
+Require Import prelude.numbers.
Notation cast_trichotomy T :=
match T with
diff --git a/theories/list.v b/theories/list.v
index 25fe629b..2b39ffe5 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3,7 +3,7 @@
(** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *)
Require Export Permutation.
-Require Export numbers base decidable option.
+Require Export prelude.numbers prelude.base prelude.decidable prelude.option.
Arguments length {_} _.
Arguments cons {_} _ _.
diff --git a/theories/listset.v b/theories/listset.v
index 5aa61a4c..147715aa 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *)
-Require Export base decidable collections list.
+Require Export prelude.base prelude.decidable prelude.collections prelude.list.
Record listset A := Listset { listset_car: list A }.
Arguments listset_car {_} _.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index 7328d21e..ab4341a8 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -3,7 +3,7 @@
(** This file implements finite as unordered lists without duplicates.
Although this implementation is slow, it is very useful as decidable equality
is the only constraint on the carrier set. *)
-Require Export base decidable collections list.
+Require Export prelude.base prelude.decidable prelude.collections prelude.list.
Record listset_nodup A := ListsetNoDup {
listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
diff --git a/theories/mapset.v b/theories/mapset.v
index d7e7c445..586a099a 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -3,7 +3,7 @@
(** This files gives an implementation of finite sets using finite maps with
elements of the unit type. Since maps enjoy extensional equality, the
constructed finite sets do so as well. *)
-Require Export fin_map_dom.
+Require Export prelude.fin_map_dom.
Record mapset (M : Type → Type) : Type :=
Mapset { mapset_car: M (unit : Type) }.
diff --git a/theories/natmap.v b/theories/natmap.v
index 320b2cb8..309520af 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -3,7 +3,7 @@
(** This files implements a type [natmap A] of finite maps whose keys range
over Coq's data type of unary natural numbers [nat]. The implementation equips
a list with a proof of canonicity. *)
-Require Import fin_maps mapset.
+Require Import prelude.fin_maps prelude.mapset.
Notation natmap_raw A := (list (option A)).
Definition natmap_wf {A} (l : natmap_raw A) :=
diff --git a/theories/nmap.v b/theories/nmap.v
index d833c6b9..1adc1a63 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [N]. *)
-Require Import pmap mapset.
-Require Export prelude fin_maps.
+Require Import prelude.pmap prelude.mapset.
+Require Export prelude.prelude prelude.fin_maps.
Local Open Scope N_scope.
diff --git a/theories/numbers.v b/theories/numbers.v
index 886d9f76..4694aaf7 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -5,7 +5,7 @@ natural numbers, and the type [Z] for integers. It also declares some useful
notations. *)
Require Export Eqdep PArith NArith ZArith NPeano.
Require Import QArith Qcanon.
-Require Export base decidable.
+Require Export prelude.base prelude.decidable.
Open Scope nat_scope.
Coercion Z.of_nat : nat >-> Z.
diff --git a/theories/option.v b/theories/option.v
index a67260f4..ed2392de 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the option
data type that are not in the Coq standard library. *)
-Require Export base tactics decidable.
+Require Export prelude.base prelude.tactics prelude.decidable.
Inductive option_reflect {A} (P : A → Prop) (Q : Prop) : option A → Type :=
| ReflectSome x : P x → option_reflect P Q (Some x)
diff --git a/theories/optionmap.v b/theories/optionmap.v
index 614f96aa..4873518b 100644
--- a/theories/optionmap.v
+++ b/theories/optionmap.v
@@ -1,7 +1,7 @@
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
-Require Import mapset.
-Require Export prelude fin_maps.
+Require Import prelude.mapset.
+Require Export prelude.prelude prelude.fin_maps.
Record optionmap (M : Type → Type) (A : Type) : Type :=
OptionMap { optionmap_None : option A; optionmap_Some : M A }.
diff --git a/theories/orders.v b/theories/orders.v
index 71568318..09ae83d0 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -3,7 +3,7 @@
(** This file collects common properties of pre-orders and semi lattices. This
theory will mainly be used for the theory on collections and finite maps. *)
Require Export Sorted.
-Require Export base decidable tactics list.
+Require Export prelude.base prelude.decidable prelude.tactics prelude.list.
(** * Arbitrary pre-, parial and total orders *)
(** Properties about arbitrary pre-, partial, and total orders. We do not use
diff --git a/theories/pmap.v b/theories/pmap.v
index 3cf4f3aa..f11ab53d 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -7,8 +7,8 @@ trees (uncompressed Patricia trees) and guarantees logarithmic-time operations.
However, we extend Leroy's implementation by packing the trees into a Sigma
type such that canonicity of representation is ensured. This is necesarry for
Leibniz equality to become extensional. *)
-Require Import PArith mapset.
-Require Export fin_maps.
+Require Import PArith prelude.mapset.
+Require Export prelude.fin_maps.
Local Open Scope positive_scope.
Local Hint Extern 0 (@eq positive _ _) => congruence.
diff --git a/theories/prelude.v b/theories/prelude.v
index 0c00f512..020b6535 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -1,16 +1,16 @@
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export
- base
- tactics
- decidable
- orders
- option
- vector
- numbers
- relations
- collections
- fin_collections
- listset
- list
- lexico.
+ prelude.base
+ prelude.tactics
+ prelude.decidable
+ prelude.orders
+ prelude.option
+ prelude.vector
+ prelude.numbers
+ prelude.relations
+ prelude.collections
+ prelude.fin_collections
+ prelude.listset
+ prelude.list
+ prelude.lexico.
diff --git a/theories/pretty.v b/theories/pretty.v
index 2bd7f21d..f76b4e3e 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -1,7 +1,7 @@
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
-Require Export numbers option.
-Require Import Ascii String relations.
+Require Export prelude.numbers prelude.option.
+Require Import Ascii String prelude.relations.
Infix "+:+" := String.append (at level 60, right associativity) : C_scope.
Arguments String.append _ _ : simpl never.
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index 6f065020..d1eab741 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -1,7 +1,7 @@
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *)
-Require Export Eqdep_dec tactics.
+Require Export Eqdep_dec prelude.tactics.
Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
diff --git a/theories/relations.v b/theories/relations.v
index da952398..cd81c198 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -5,7 +5,7 @@ These are particularly useful as we define the operational semantics as a
small step semantics. This file defines a hint database [ars] containing
some theorems on abstract rewriting systems. *)
Require Import Wf_nat.
-Require Export tactics base.
+Require Export prelude.tactics prelude.base.
(** * Definitions *)
Section definitions.
diff --git a/theories/sets.v b/theories/sets.v
index 9e3d2d21..bd80b8ee 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1,7 +1,7 @@
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *)
-Require Export prelude.
+Require Export prelude.prelude.
Record set (A : Type) : Type := mkSet { set_car : A → Prop }.
Arguments mkSet {_} _.
@@ -28,4 +28,4 @@ Instance set_join : MJoin set := λ A (XX : set (set A)),
Instance set_collection_monad : CollectionMonad set.
Proof. by split; try apply _. Qed.
-Global Opaque set_union set_intersection.
\ No newline at end of file
+Global Opaque set_union set_intersection.
diff --git a/theories/streams.v b/theories/streams.v
index af231e02..c660562c 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -1,6 +1,6 @@
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
-Require Export tactics.
+Require Export prelude.tactics.
CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
Arguments scons {_} _ _.
diff --git a/theories/stringmap.v b/theories/stringmap.v
index c519eff8..b7fafeec 100644
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -4,8 +4,8 @@
range over Coq's data type of strings [string]. The implementation uses radix-2
search trees (uncompressed Patricia trees) as implemented in the file [pmap]
and guarantees logarithmic-time operations. *)
-Require Export fin_maps pretty.
-Require Import Ascii String list pmap mapset.
+Require Export prelude.fin_maps prelude.pretty.
+Require Import Ascii String prelude.list prelude.pmap prelude.mapset.
(** * Encoding and decoding *)
(** In order to reuse or existing implementation of radix-2 search trees over
diff --git a/theories/tactics.v b/theories/tactics.v
index 70f4f941..ece653ff 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -3,7 +3,7 @@
(** This file collects general purpose tactics that are used throughout
the development. *)
Require Export Psatz.
-Require Export base.
+Require Export prelude.base.
Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x.
Proof. intros ->; reflexivity. Qed.
diff --git a/theories/vector.v b/theories/vector.v
index 6cacf063..da77f8fd 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -5,7 +5,7 @@
definitions from the standard library, but renames or changes their notations,
so that it becomes more consistent with the naming conventions in this
development. *)
-Require Import list finite.
+Require Import prelude.list prelude.finite.
Open Scope vector_scope.
(** * The fin type *)
diff --git a/theories/zmap.v b/theories/zmap.v
index f91c7fb4..04f016e1 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [Z]. *)
-Require Import pmap mapset.
-Require Export prelude fin_maps.
+Require Import prelude.pmap prelude.mapset.
+Require Export prelude.prelude prelude.fin_maps.
Local Open Scope Z_scope.
Record Zmap (A : Type) : Type :=
--
GitLab