Coq -> Stdlib/Rocq renaming

.nix/coq-overlays/equations/default.nix

@@ -63,5 +63,5 @@ with lib; (mkCoqDerivation {
     maintainers = with maintainers; [ jwiegley ];
   };
 }).overrideAttrs (o: {
-  preBuild = "coq_makefile -f _CoqProject -o Makefile${optionalString (versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
+  preBuild = "rocq makefile -f _CoqProject -o Makefile${optionalString (versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
 })

DOC.md

@@ -28,7 +28,7 @@ inserts some JMeq and UIP axioms silently, whereas we try to keep the developmen
 You can use `Equations` to do some dependent induction (`dependent induction`,
 `dependent destruction`, `depelim`). You may need to add:
 ```
-Require Import Equations.Prop.DepElim.
+From Equations.Prop Require Import DepElim.
 ```
 
 ## ident vs. qualid. vs kername

common/Makefile

@@ -25,7 +25,7 @@ mrproper:
 	rm -f Makefile.coq
 
 Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.coq
+	rocq makefile -f _CoqProject -o Makefile.coq
 
 .merlin: Makefile.coq
 	$(MAKE) -f $< $@

common/theories/BasicAst.v

@@ -1,8 +1,8 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect Morphisms Orders Setoid.
+From Stdlib Require Import ssreflect Morphisms Orders Setoid.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Export Kernames.
-From Coq Require Floats.SpecFloat.
+From Stdlib Require Floats.SpecFloat.
 From Equations Require Import Equations.
 
 (** Identifiers that are allowed to be anonymous (i.e. "_" in concrete syntax). *)

common/theories/EnvMap.v

@@ -1,6 +1,6 @@
 
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect RelationClasses OrderedTypeAlt FMapAVL FMapFacts.
+From Stdlib Require Import ssreflect RelationClasses OrderedTypeAlt FMapAVL FMapFacts.
 From MetaCoq.Utils Require Import utils String2pos CanonicalTries.
 From MetaCoq.Common Require Import config uGraph Reflect BasicAst Kernames.
 From Equations Require Import Equations.

common/theories/Environment.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect ssrbool ssrfun Morphisms Setoid.
+From Stdlib Require Import ssreflect ssrbool ssrfun Morphisms Setoid.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Primitive Universes.
 From Equations.Prop Require Import Classes EqDecInstances.
@@ -218,7 +218,7 @@ Module Environment (T : Term).
        decl_body := decl_body x;
        decl_type := decl_type x |}.
 
-  (** Count the number of assumptions in a context (i.e. declarations that do not 
+  (** Count the number of assumptions in a context (i.e. declarations that do not
       contain a body). *)
   Fixpoint context_assumptions (Γ : context) : nat :=
     match Γ with
@@ -327,7 +327,7 @@ Module Environment (T : Term).
         `ind_bodies ,,, ind_params ,,, cstr_args |- cstr_indices`. *)
     cstr_indices : list term;
     (** Full type of the constructor, which can depend on the inductives in the same block :
-        `ind_bodies |- cstr_type`. This should be equal to 
+        `ind_bodies |- cstr_type`. This should be equal to
         `forall ind_params cstr_args, I ind_params cstr_indices` *)
     cstr_type : term;
     (** Number of arguments of the constructor, _without_ let-in arguments and _without_ parameters.
@@ -341,7 +341,7 @@ Module Environment (T : Term).
     proj_name : ident;
     (** Relevance of the projection. *)
     proj_relevance : relevance;
-    (** Type of the projection, wich can depend on the parameters of the inductive 
+    (** Type of the projection, wich can depend on the parameters of the inductive
         and on the object we are projecting from : `ind_params ,,, x |- proj_type`. *)
     proj_type : term;
   }.
@@ -365,21 +365,21 @@ Module Environment (T : Term).
   (** Data associated to a single inductive in a mutual inductive block. *)
   Record one_inductive_body := {
     (** Name of the inductive, without the module path. *)
-    ind_name : ident; 
+    ind_name : ident;
     (** Indices of the inductive, which can depend on the parameters :
         `ind_params |- ind_indices`. *)
     ind_indices : context;
-    (** Sort of the inductive. *) 
-    ind_sort : Sort.t; 
+    (** Sort of the inductive. *)
+    ind_sort : Sort.t;
     (** Full type of the inductive. This should be equal to
         `forall ind_params ind_indices, tSort ind_sort` *)
-    ind_type : term; 
+    ind_type : term;
     (** Allowed eliminations for the inductive. *)
-    ind_kelim : allowed_eliminations; 
+    ind_kelim : allowed_eliminations;
     (** Constructors of the inductive. Order is important. *)
     ind_ctors : list constructor_body;
     (** Names and types of primitive projections, if any. *)
-    ind_projs : list projection_body; 
+    ind_projs : list projection_body;
     (** Relevance of the inductive. *)
     ind_relevance : relevance }.
 

common/theories/EnvironmentReflect.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect ssrbool ssrfun Morphisms Setoid.
+From Stdlib Require Import ssreflect ssrbool ssrfun Morphisms Setoid.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Primitive Universes Environment Reflect.
 From Equations.Prop Require Import Classes EqDecInstances.

common/theories/EnvironmentTyping.v

@@ -1,6 +1,6 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect ssrbool.
-From Coq Require CMorphisms CRelationClasses.
+From Stdlib Require Import ssreflect ssrbool.
+From Stdlib Require CMorphisms CRelationClasses.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config BasicAst Universes Environment Primitive.
 From Equations Require Import Equations.

common/theories/Kernames.v

@@ -1,8 +1,8 @@
 
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import Lia MSetList OrderedTypeAlt OrderedTypeEx FMapAVL FMapFacts MSetAVL MSetFacts MSetProperties.
+From Stdlib Require Import Lia MSetList OrderedTypeAlt OrderedTypeEx FMapAVL FMapFacts MSetAVL MSetFacts MSetProperties.
 From MetaCoq.Utils Require Import utils MCMSets MCFSets.
-From Coq Require Import ssreflect.
+From Stdlib Require Import ssreflect.
 From Equations Require Import Equations.
 
 Local Open Scope string_scope2.

common/theories/Primitive.v

@@ -1,6 +1,6 @@
 (* Primitive types *)
 
-From Coq Require Import Uint63 PrimFloat SpecFloat FloatOps ZArith HexadecimalString.
+From Stdlib Require Import Uint63 PrimFloat SpecFloat FloatOps ZArith HexadecimalString.
 From MetaCoq.Utils Require Import bytestring MCString.
 Local Open Scope bs.
 

common/theories/Reflect.v

@@ -1,9 +1,9 @@
 (* Distributed under the terms of the MIT license. *)
 (* For primitive integers and floats  *)
-From Coq Require Numbers.Cyclic.Int63.Uint63 Floats.PrimFloat Floats.FloatAxioms.
+From Stdlib Require Numbers.Cyclic.Int63.Uint63 Floats.PrimFloat Floats.FloatAxioms.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Universes Kernames.
-Require Import ssreflect.
+From Stdlib Require Import ssreflect.
 From Equations Require Import Equations.
 
 #[program,global] Instance reflect_prim_int : ReflectEq Numbers.Cyclic.Int63.Uint63.int :=
@@ -260,7 +260,7 @@ Proof.
   f_equal. apply uip.
 Qed.
 
-Require Import RelationClasses.
+From Stdlib Require Import RelationClasses.
 
 Lemma constraint_lt_irrel (x y : UnivConstraint.t) (l l' : UnivConstraint.lt_ x y) : l = l'.
 Proof.

common/theories/Transform.v

@@ -3,7 +3,7 @@
 (** Generic transofmations from one language to another,
     preserving an evaluation relation up-to some observational equality. *)
 
-From Coq Require Import Program ssreflect ssrbool.
+From Stdlib Require Import Program ssreflect ssrbool.
 From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils.
 Import bytestring.

common/theories/Universes.v

@@ -1,8 +1,8 @@
-From Coq Require Import OrdersAlt MSetList MSetAVL MSetFacts MSetProperties MSetDecide FMapAVL.
+From Stdlib Require Import OrdersAlt MSetList MSetAVL MSetFacts MSetProperties MSetDecide FMapAVL.
 From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils MCMSets MCFSets.
 From MetaCoq.Common Require Import BasicAst config.
-Require Import ssreflect.
+From Stdlib Require Import ssreflect.
 
 Local Open Scope nat_scope.
 Local Open Scope string_scope2.

common/theories/UniversesDec.v

@@ -1,4 +1,4 @@
-From Coq Require Import PArith NArith ZArith Lia.
+From Stdlib Require Import PArith NArith ZArith Lia.
 From MetaCoq.Utils Require Import MCList MCOption MCUtils.
 From MetaCoq.Common Require Import uGraph.
 From MetaCoq.Common Require Import Universes.

common/theories/uGraph.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-Require Import ssreflect ssrbool OrderedTypeAlt MSetAVL MSetFacts MSetProperties MSetDecide Morphisms.
+From Stdlib Require Import ssreflect ssrbool OrderedTypeAlt MSetAVL MSetFacts MSetProperties MSetDecide Morphisms.
 From MetaCoq.Utils Require Import utils wGraph.
 From MetaCoq.Common Require Import config Universes.
 From Equations.Prop Require Import DepElim.
@@ -3079,7 +3079,7 @@ Proof.
 Qed.
 
 
-Require Import SetoidTactics.
+From Stdlib Require Import SetoidTactics.
 
 #[global] Instance is_graph_of_uctx_proper {cf : checker_flags} G : Proper ((=_cs) ==> iff) (is_graph_of_uctx G).
 Proof.

configure.sh

@@ -8,11 +8,9 @@ make -f Makefile mrproper
 # should already be available in $(COQMF_LIB)/user-contrib/MetaCoq/*
 # For local builds, we set specific dependencies of each subproject in */metacoq-config
 
-# CWD=`pwd`
-
-if command -v coqc >/dev/null 2>&1
+if command -v rocq >/dev/null 2>&1
 then
-    COQLIB=` coqc -where | tr -d '\r' | tr '\\\\' '/'`
+    COQLIB=` rocq c -where | tr -d '\r' | tr '\\\\' '/'`
 
     if [[ "$1" = "local" ]] || [[ "$1" = "--enable-local" ]] || [[ "$1" = "--enable-quick" ]]
     then
@@ -78,5 +76,5 @@ then
     echo ${PLUGIN_DEMO_DEPS} >> test-suite/plugin-demo/metacoq-config
 
 else
-    echo "Error: coqc not found in path"
+    echo "Error: rocq not found in path"
 fi

erasure-plugin/Makefile

@@ -9,12 +9,12 @@ _CoqProject: _CoqProject.in metacoq-config
 	cat _CoqProject.in >> _CoqProject
 
 Makefile.plugin: _PluginProject
-	coq_makefile -f _PluginProject -o Makefile.plugin $(DEPS)
+	rocq makefile -f _PluginProject -o Makefile.plugin $(DEPS)
 # Avoid conflicting dependency file creation for the template plugin
 	sed -e s/coqdeps/coqdeps.plugin/g Makefile.plugin > Makefile.plugin.tmp && mv -f Makefile.plugin.tmp Makefile.plugin
 
 Makefile.erasureplugin: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.erasureplugin $(DEPS)
+	rocq makefile -f _CoqProject -o Makefile.erasureplugin $(DEPS)
 
 theory: Makefile.erasureplugin
 	$(MAKE) -f Makefile.erasureplugin

erasure-plugin/clean_extraction.sh

@@ -1,5 +1,7 @@
 #!/usr/bin/env bash
 
+SED=`which gsed || which sed`
+
 echo "Cleaning result of extraction"
 
 if [ ! -d "src" ]
@@ -9,7 +11,7 @@ fi
 
 shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
 
-files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | ${SED} -e s/gen-src/src/`
 
 if [[ ! -f "src/metacoq_erasure_plugin.cmxs" ||
            "src/metacoq_erasure_plugin.cmxs" -ot "theories/Extraction.vo" ]]

erasure-plugin/theories/ETransform.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import Program ssreflect ssrbool.
+From Stdlib Require Import Program ssreflect ssrbool.
 From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import Environment Transform config BasicAst uGraph.

erasure-plugin/theories/Erasure.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import Program ssreflect ssrbool.
+From Stdlib Require Import Program ssreflect ssrbool.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import Transform config.
 From MetaCoq.Template Require Import EtaExpand TemplateProgram.

erasure-plugin/theories/ErasureCorrectness.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import Program ssreflect ssrbool.
+From Stdlib Require Import Program ssreflect ssrbool.
 From MetaCoq.Common Require Import Transform config.
 From MetaCoq.Utils Require Import bytestring utils.
 From MetaCoq.PCUIC Require PCUICAst PCUICAstUtils PCUICProgram.
@@ -428,7 +428,7 @@ Proof.
 Qed.
 
 Import MetaCoq.Common.Transform.
-From Coq Require Import Morphisms.
+From Stdlib Require Import Morphisms.
 
 Module ETransformPresFO.
   Section Opt.

erasure-plugin/theories/Loader.v

@@ -1,4 +1,4 @@
-Require Import String.
+From Stdlib Require Import String.
 From MetaCoq.Template Require ExtractableLoader.
 
 Declare ML Module "coq-metacoq-erasure.plugin".

erasure/Makefile

@@ -5,7 +5,7 @@ _CoqProject: _CoqProject.in metacoq-config
 	cat _CoqProject.in >> _CoqProject
 
 Makefile.erasure: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.erasure $(DEPS)
+	rocq makefile -f _CoqProject -o Makefile.erasure $(DEPS)
 
 theory: Makefile.erasure
 	$(MAKE) -f Makefile.erasure

erasure/theories/EArities.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect ssrbool.
+From Stdlib Require Import ssreflect ssrbool.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
@@ -16,7 +16,7 @@ From MetaCoq.Erasure Require Import Extract.
 
 Notation "Σ ⊢p s ⇓ t" := (eval Σ s t) (at level 50, s, t at next level) : type_scope.
 
-Require Import Program.
+From Stdlib Require Import Program.
 From Equations Require Import Equations.
 
 Local Existing Instance extraction_checker_flags.

erasure/theories/EAstUtils.v

@@ -3,7 +3,7 @@ From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Kernames.
 From MetaCoq.Erasure Require Import EPrimitive EAst.
-Require Import ssreflect ssrbool.
+From Stdlib Require Import ssreflect ssrbool.
 
 Global Hint Resolve app_tip_nil : core.
 

erasure/theories/EBeta.v

@@ -1,5 +1,5 @@
-From Coq Require Import List.
-From Coq Require Import String.
+From Stdlib Require Import List.
+From Stdlib Require Import String.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst.
 From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils ELiftSubst EProgram.

erasure/theories/ECSubst.v

@@ -1,9 +1,9 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import Program.
+From Stdlib Require Import Program.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction ELiftSubst.
 
-Require Import ssreflect ssrbool.
+From Stdlib Require Import ssreflect ssrbool.
 From Equations Require Import Equations.
 
 

erasure/theories/ECoInductiveToInductive.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import Utf8 Program.
+From Stdlib Require Import Utf8 Program.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Kernames.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
@@ -21,7 +21,7 @@ Import MCMonadNotation.
 From Equations Require Import Equations.
 Set Equations Transparent.
 Local Set Keyed Unification.
-Require Import ssreflect ssrbool.
+From Stdlib Require Import ssreflect ssrbool.
 
 (** We assumes [Prop </= Type] and universes are checked correctly in the following. *)
 Local Existing Instance extraction_checker_flags.

erasure/theories/EConstructorsAsBlocks.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import Utf8 Program.
+From Stdlib Require Import Utf8 Program.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Kernames BasicAst EnvMap.
 From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EArities
@@ -13,7 +13,7 @@ Import MCMonadNotation.
 From Equations Require Import Equations.
 Set Equations Transparent.
 Local Set Keyed Unification.
-From Coq Require Import ssreflect ssrbool.
+From Stdlib Require Import ssreflect ssrbool.
 
 (** We assume [Prop </= Type] and universes are checked correctly in the following. *)
 (* Local Existing Instance extraction_checker_flags. *)

erasure/theories/EDeps.v

@@ -1,4 +1,4 @@
-From Coq Require Import Arith List.
+From Stdlib Require Import Arith List.
 From Equations Require Import Equations.
 From MetaCoq.PCUIC Require Import
      PCUICPrimitive PCUICAst PCUICAstUtils PCUICTyping PCUICInversion PCUICWeakeningEnv PCUICWeakeningEnvTyp.

erasure/theories/EEnvMap.v

@@ -1,4 +1,4 @@
-From Coq Require Import ssreflect ssrbool Morphisms Setoid ProofIrrelevance.
+From Stdlib Require Import ssreflect ssrbool Morphisms Setoid ProofIrrelevance.
 From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import Kernames EnvMap BasicAst.