From 8dc73363e511dfa4f2a483e5ada0f6960863a672 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.
---
SConstruct | 4 ++--
iris/agree.v | 2 +-
iris/auth.v | 2 +-
iris/cmra.v | 2 +-
iris/cofe.v | 2 +-
iris/cofe_instances.v | 4 ++--
iris/cofe_solver.v | 2 +-
iris/dra.v | 2 +-
iris/excl.v | 2 +-
iris/logic.v | 2 +-
iris/ra.v | 2 +-
iris/sts.v | 4 ++--
prelude/assoc.v | 4 ++--
prelude/collections.v | 2 +-
prelude/countable.v | 2 +-
prelude/decidable.v | 2 +-
prelude/error.v | 2 +-
prelude/fin_collections.v | 4 ++--
prelude/fin_map_dom.v | 2 +-
prelude/fin_maps.v | 2 +-
prelude/finite.v | 2 +-
prelude/hashset.v | 4 ++--
prelude/lexico.v | 2 +-
prelude/list.v | 2 +-
prelude/listset.v | 2 +-
prelude/listset_nodup.v | 2 +-
prelude/mapset.v | 2 +-
prelude/natmap.v | 2 +-
prelude/nmap.v | 4 ++--
prelude/numbers.v | 2 +-
prelude/option.v | 2 +-
prelude/optionmap.v | 4 ++--
prelude/orders.v | 2 +-
prelude/pmap.v | 4 ++--
prelude/prelude.v | 26 +++++++++++++-------------
prelude/pretty.v | 4 ++--
prelude/proof_irrel.v | 2 +-
prelude/relations.v | 2 +-
prelude/sets.v | 4 ++--
prelude/streams.v | 2 +-
prelude/stringmap.v | 4 ++--
prelude/tactics.v | 2 +-
prelude/vector.v | 2 +-
prelude/zmap.v | 4 ++--
44 files changed, 69 insertions(+), 69 deletions(-)
diff --git a/SConstruct b/SConstruct
index 9572d77d8..1c23caeec 100644
--- a/SConstruct
+++ b/SConstruct
@@ -3,7 +3,7 @@
import os, glob, string
modules = ["prelude", "iris"]
-Rs = '-R . iris'
+Rs = ' '.join(['-Q ' + x + ' ' + x for x in modules])
env = DefaultEnvironment(ENV = os.environ,tools=['default', 'Coq'], COQFLAGS=Rs)
# Coq dependencies
@@ -15,4 +15,4 @@ ParseDepends('deps')
for v in vs: env.Coq(v)
# Coqidescript
-env.CoqIdeScript('coqidescript', [])
+env.CoqIdeScript('coqidescript', [], COQFLAGS=Rs)
diff --git a/iris/agree.v b/iris/agree.v
index 6fa31f5f1..d60df048f 100644
--- a/iris/agree.v
+++ b/iris/agree.v
@@ -1,4 +1,4 @@
-Require Export cmra.
+Require Export iris.cmra.
Local Hint Extern 10 (_ ≤ _) => omega.
Record agree A `{Dist A} := Agree {
diff --git a/iris/auth.v b/iris/auth.v
index 9e55f85f8..f0e9b054e 100644
--- a/iris/auth.v
+++ b/iris/auth.v
@@ -1,4 +1,4 @@
-Require Export excl.
+Require Export iris.excl.
Local Arguments disjoint _ _ !_ !_ /.
Local Arguments included _ _ !_ !_ /.
diff --git a/iris/cmra.v b/iris/cmra.v
index 8a4f008a6..28afd745e 100644
--- a/iris/cmra.v
+++ b/iris/cmra.v
@@ -1,4 +1,4 @@
-Require Export ra cofe cofe_instances.
+Require Export iris.ra iris.cofe.
Class ValidN (A : Type) := validN : nat → A → Prop.
Instance: Params (@validN) 3.
diff --git a/iris/cofe.v b/iris/cofe.v
index 9b538adb3..ee557f4bb 100644
--- a/iris/cofe.v
+++ b/iris/cofe.v
@@ -1,4 +1,4 @@
-Require Export prelude.
+Require Export prelude.prelude.
Obligation Tactic := idtac.
(** Unbundeled version *)
diff --git a/iris/cofe_instances.v b/iris/cofe_instances.v
index d67e02dd4..76f14b6b6 100644
--- a/iris/cofe_instances.v
+++ b/iris/cofe_instances.v
@@ -1,5 +1,5 @@
-Require Export cofe.
-Require Import fin_maps pmap nmap zmap stringmap.
+Require Export iris.cofe.
+Require Import prelude.fin_maps prelude.pmap prelude.nmap prelude.zmap prelude.stringmap.
(** Discrete cofe *)
Section discrete_cofe.
diff --git a/iris/cofe_solver.v b/iris/cofe_solver.v
index 89a1d855f..59a85698f 100644
--- a/iris/cofe_solver.v
+++ b/iris/cofe_solver.v
@@ -1,4 +1,4 @@
-Require Export cofe.
+Require Export iris.cofe.
Section solver.
Context (F : cofeT → cofeT → cofeT).
diff --git a/iris/dra.v b/iris/dra.v
index 34fc07bec..b7f573f0c 100644
--- a/iris/dra.v
+++ b/iris/dra.v
@@ -1,4 +1,4 @@
-Require Export ra.
+Require Export iris.ra.
(** From disjoint pcm *)
Record validity {A} (P : A → Prop) : Type := Validity {
diff --git a/iris/excl.v b/iris/excl.v
index 910870ceb..7a82fd559 100644
--- a/iris/excl.v
+++ b/iris/excl.v
@@ -1,4 +1,4 @@
-Require Export cmra.
+Require Export iris.cmra.
Local Arguments disjoint _ _ !_ !_ /.
Local Arguments included _ _ !_ !_ /.
diff --git a/iris/logic.v b/iris/logic.v
index fdc73daff..ae180da61 100644
--- a/iris/logic.v
+++ b/iris/logic.v
@@ -1,4 +1,4 @@
-Require Import cmra cofe_instances.
+Require Import iris.cmra.
Local Hint Extern 1 (_ ≼ _) => etransitivity; [eassumption|].
Local Hint Extern 1 (_ ≼ _) => etransitivity; [|eassumption].
Local Hint Extern 10 (_ ≤ _) => omega.
diff --git a/iris/ra.v b/iris/ra.v
index 38c082688..35d783676 100644
--- a/iris/ra.v
+++ b/iris/ra.v
@@ -1,4 +1,4 @@
-Require Export collections relations.
+Require Export prelude.collections prelude.relations.
Class Valid (A : Type) := valid : A → Prop.
Instance: Params (@valid) 2.
diff --git a/iris/sts.v b/iris/sts.v
index ac7619d56..f9f7e5940 100644
--- a/iris/sts.v
+++ b/iris/sts.v
@@ -1,5 +1,5 @@
-Require Export ra.
-Require Import sets stringmap dra.
+Require Export iris.ra.
+Require Import prelude.sets prelude.stringmap iris.dra.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments unit _ _ !_ /.
diff --git a/prelude/assoc.v b/prelude/assoc.v
index c9e609ba1..3b8730a5f 100644
--- a/prelude/assoc.v
+++ b/prelude/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/prelude/collections.v b/prelude/collections.v
index eaff59e01..7caafe69d 100644
--- a/prelude/collections.v
+++ b/prelude/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/prelude/countable.v b/prelude/countable.v
index c62eb2351..628aa5523 100644
--- a/prelude/countable.v
+++ b/prelude/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/prelude/decidable.v b/prelude/decidable.v
index 96720b24e..184372c8b 100644
--- a/prelude/decidable.v
+++ b/prelude/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/prelude/error.v b/prelude/error.v
index 46fe0c578..0eb6c33f5 100644
--- a/prelude/error.v
+++ b/prelude/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/prelude/fin_collections.v b/prelude/fin_collections.v
index f4e63f636..28591e60a 100644
--- a/prelude/fin_collections.v
+++ b/prelude/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/prelude/fin_map_dom.v b/prelude/fin_map_dom.v
index bbdbb8ea6..f69fabecb 100644
--- a/prelude/fin_map_dom.v
+++ b/prelude/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/prelude/fin_maps.v b/prelude/fin_maps.v
index b77edcd47..7e12d0e4e 100644
--- a/prelude/fin_maps.v
+++ b/prelude/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/prelude/finite.v b/prelude/finite.v
index 9aa8a459e..782400116 100644
--- a/prelude/finite.v
+++ b/prelude/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/prelude/hashset.v b/prelude/hashset.v
index 345ba837a..f517f0e76 100644
--- a/prelude/hashset.v
+++ b/prelude/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/prelude/lexico.v b/prelude/lexico.v
index e36b552ad..31ddc33ba 100644
--- a/prelude/lexico.v
+++ b/prelude/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/prelude/list.v b/prelude/list.v
index 25fe629b7..2b39ffe56 100644
--- a/prelude/list.v
+++ b/prelude/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/prelude/listset.v b/prelude/listset.v
index 5aa61a4cd..147715aa2 100644
--- a/prelude/listset.v
+++ b/prelude/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/prelude/listset_nodup.v b/prelude/listset_nodup.v
index 7328d21ef..ab4341a83 100644
--- a/prelude/listset_nodup.v
+++ b/prelude/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/prelude/mapset.v b/prelude/mapset.v
index d7e7c445e..586a099ae 100644
--- a/prelude/mapset.v
+++ b/prelude/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/prelude/natmap.v b/prelude/natmap.v
index 320b2cb87..309520af7 100644
--- a/prelude/natmap.v
+++ b/prelude/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/prelude/nmap.v b/prelude/nmap.v
index d833c6b90..1adc1a636 100644
--- a/prelude/nmap.v
+++ b/prelude/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/prelude/numbers.v b/prelude/numbers.v
index 886d9f768..4694aaf73 100644
--- a/prelude/numbers.v
+++ b/prelude/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/prelude/option.v b/prelude/option.v
index a67260f46..ed2392de0 100644
--- a/prelude/option.v
+++ b/prelude/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/prelude/optionmap.v b/prelude/optionmap.v
index 614f96aa2..4873518b8 100644
--- a/prelude/optionmap.v
+++ b/prelude/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/prelude/orders.v b/prelude/orders.v
index 715683181..09ae83d09 100644
--- a/prelude/orders.v
+++ b/prelude/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/prelude/pmap.v b/prelude/pmap.v
index 3cf4f3aa9..f11ab53d0 100644
--- a/prelude/pmap.v
+++ b/prelude/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/prelude/prelude.v b/prelude/prelude.v
index 0c00f5125..020b6535b 100644
--- a/prelude/prelude.v
+++ b/prelude/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/prelude/pretty.v b/prelude/pretty.v
index 2bd7f21d6..f76b4e3ee 100644
--- a/prelude/pretty.v
+++ b/prelude/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/prelude/proof_irrel.v b/prelude/proof_irrel.v
index 6f065020a..d1eab7410 100644
--- a/prelude/proof_irrel.v
+++ b/prelude/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/prelude/relations.v b/prelude/relations.v
index da9523984..cd81c198f 100644
--- a/prelude/relations.v
+++ b/prelude/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/prelude/sets.v b/prelude/sets.v
index 9e3d2d210..bd80b8eeb 100644
--- a/prelude/sets.v
+++ b/prelude/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/prelude/streams.v b/prelude/streams.v
index af231e02f..c660562cf 100644
--- a/prelude/streams.v
+++ b/prelude/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/prelude/stringmap.v b/prelude/stringmap.v
index c519eff82..b7fafeeca 100644
--- a/prelude/stringmap.v
+++ b/prelude/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/prelude/tactics.v b/prelude/tactics.v
index 70f4f9412..ece653ff4 100644
--- a/prelude/tactics.v
+++ b/prelude/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/prelude/vector.v b/prelude/vector.v
index 6cacf063e..da77f8fd9 100644
--- a/prelude/vector.v
+++ b/prelude/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/prelude/zmap.v b/prelude/zmap.v
index f91c7fb4e..04f016e1d 100644
--- a/prelude/zmap.v
+++ b/prelude/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