Merge pull request rocq-archive#422 from proux01/coq_19310

Adapt to coq/coq#19310
proux01 · Sep 10, 2024 · 652a8cc · 652a8cc
2 parents feb42b7 + 4bcf97e
commit 652a8cc
Show file tree

Hide file tree

Showing 8 changed files with 16 additions and 16 deletions.
diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml
@@ -75,7 +75,7 @@ exception CannotSaveVo
  *   [@@deriving sexp]
  *)
 
-(* XXX: Use a module here to have Coq.String etc...? *)
+(* XXX: Use a module here to have Stdlib.String etc...? *)
 type coq_object =
   | CoqString    of string
   | CoqSList     of string list
@@ -891,7 +891,7 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t =
   coq_protect st @@ fun () -> match cmd with
   | NewDoc opts   ->
     let stm_options = Stm.AsyncOpts.default_opts in
-    let require_libs = Option.default [{Coqargs.lib="Coq.Init.Prelude"; prefix=None; export=Some Lib.Export;}] opts.require_libs in
+    let require_libs = Option.default [{Coqargs.lib="Stdlib.Init.Prelude"; prefix=None; export=Some Lib.Export;}] opts.require_libs in
     Stm.init_process stm_options;
     let ndoc = { Stm.doc_type = Stm.(Interactive opts.top_name)
                ; injections = List.map (fun x -> Coqargs.RequireInjection x) require_libs

diff --git a/sertop/comp_common.ml b/sertop/comp_common.ml
@@ -79,7 +79,7 @@ let create_document ~debug ~set_impredicative_set ~disallow_sprop ~ml_path ~load
     else stm_options
   in
 
-  let injections = [Coqargs.RequireInjection {lib="Coq.Init.Prelude"; prefix=None; export=Some Lib.Import;}] in
+  let injections = [Coqargs.RequireInjection {lib="Stdlib.Init.Prelude"; prefix=None; export=Some Lib.Import;}] in
   Stm.init_process stm_options;
   let ndoc = { Stm.doc_type = Stm.VoDoc in_file
              ; injections

diff --git a/sertop/sertop_arg.ml b/sertop/sertop_arg.ml
@@ -25,7 +25,7 @@ let coqlib_from_env_or_config =
 
 [@@@ocaml.warning "-44-45"]
 let prelude =
-  let doc = "Load Coq.Init.Prelude from $(docv); plugins/ and theories/ should live there." in
+  let doc = "Load Stdlib.Init.Prelude from $(docv); plugins/ and theories/ should live there." in
   Arg.(value & opt string coqlib_from_env_or_config & info ["coqlib"] ~docv:"COQPATH" ~doc)
 
 let require_lib =

diff --git a/sertop/sertop_sexp.ml b/sertop/sertop_sexp.ml
@@ -234,7 +234,7 @@ let ser_loop ser_opts =
 
   let injections =
     if ser_opts.no_prelude then []
-    else [Coqargs.RequireInjection {lib="Coq.Init.Prelude"; prefix=None; export=Some Lib.Import;}] in
+    else [Coqargs.RequireInjection {lib="Stdlib.Init.Prelude"; prefix=None; export=Some Lib.Import;}] in
 
   let stm_options = Sertop_init.process_stm_flags ser_opts.async in
   Stm.init_process stm_options;

diff --git a/tests/genarg/extraction.v b/tests/genarg/extraction.v
@@ -1,4 +1,4 @@
-Require Coq.extraction.Extraction.
+Require Stdlib.extraction.Extraction.
 
 Extraction Language Haskell.
 

diff --git a/tests/genarg/libTactics.v b/tests/genarg/libTactics.v
@@ -44,7 +44,7 @@
 
 Set Implicit Arguments.
 
-Require Import Coq.Lists.List.
+Require Import Stdlib.Lists.List.
 
 
 (* ********************************************************************** *)
@@ -370,7 +370,7 @@ Ltac fast_rm_inside E :=
     Note: the tactic [number_to_nat] is extended in [LibInt] to
     take into account the [int] type, alias for [Z]. *)
 
-Require Coq.Numbers.BinNums Coq.ZArith.BinInt.
+Require Stdlib.Numbers.BinNums Stdlib.ZArith.BinInt.
 
 Definition ltac_int_to_nat (x:BinInt.Z) : nat :=
   match x with
@@ -2519,7 +2519,7 @@ Tactic Notation "subst_eq" constr(E) :=
 (* ---------------------------------------------------------------------- *)
 (** ** Tactics to work with proof irrelevance *)
 
-Require Import Coq.Logic.ProofIrrelevance.
+Require Import Stdlib.Logic.ProofIrrelevance.
 
 (** [pi_rewrite E] replaces [E] of type [Prop] with a fresh
     unification variable, and is thus a practical way to
@@ -3098,7 +3098,7 @@ Tactic Notation "cases_if'" :=
     [inductions E gen X1 .. XN] is a shorthand for
     [dependent induction E generalizing X1 .. XN]. *)
 
-Require Import Coq.Program.Equality.
+Require Import Stdlib.Program.Equality.
 
 Ltac inductions_post :=
   unfold eq' in *.
@@ -3189,7 +3189,7 @@ Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
     judgment that includes a counter for the maximal height
     (see LibTacticsDemos for an example) *)
 
-Require Import Coq.Arith.Compare_dec.
+Require Import Stdlib.Arith.Compare_dec.
 Require Import Lia.
 
 Lemma induct_height_max2 : forall n1 n2 : nat,
@@ -4166,7 +4166,7 @@ Tactic Notation "exists" "~" constr(T1) "," constr(T2) "," constr(T3) ","
     same as for light automation.
 
     Exception: use [subs*] instead of [subst*] if you
-    import the library [Coq.Classes.Equivalence]. *)
+    import the library [Stdlib.Classes.Equivalence]. *)
 
 Tactic Notation "equates" "*" constr(E) :=
    equates E; auto_star.
@@ -5007,7 +5007,7 @@ Open Scope nat_scope.
 
 (** [exists T1 ... TN, P] is a shorthand for
     [exists T1, ..., exists TN, P]. Note that
-    [Coq.Program.Syntax] already defines exists
+    [Stdlib.Program.Syntax] already defines exists
     for arity up to 4. *)
 
 Notation "'exists' x1 ',' P" :=

diff --git a/tests/sername/nat_add.out b/tests/sername/nat_add.out
@@ -1,2 +1,2 @@
-Nat.add: "nat -> nat -> nat" (Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Prod((binder_name(Name(Id m)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()())))))) ((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))))(loc()))))(loc()))
-Nat.mul: "nat -> nat -> nat" (Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Prod((binder_name(Name(Id m)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()()))))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0)(Instance(()())))))) ((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))())0))()))(loc()))))(loc()))))(loc()))
+Nat.add: "nat -> nat -> nat" (Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0)(Instance(()()))))(Prod((binder_name(Name(Id m)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0)(Instance(()()))))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0)(Instance(()())))))) ((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0))()))(loc()))((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0))()))(loc()))((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0))()))(loc()))))(loc()))))(loc()))
+Nat.mul: "nat -> nat -> nat" (Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0)(Instance(()()))))(Prod((binder_name(Name(Id m)))(binder_relevance Relevant))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0)(Instance(()()))))(Ind(((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0)(Instance(()())))))) ((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0))()))(loc()))((v(GProd Anonymous()Explicit((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0))()))(loc()))((v(GRef(IndRef((MutInd(KerName(MPfile(DirPath((Id Datatypes)(Id Init)(Id Stdlib))))(Id nat))())0))()))(loc()))))(loc()))))(loc()))
diff --git a/tests/sertop/full_env.in b/tests/sertop/full_env.in
@@ -1,4 +1,4 @@
-("query0"("Add"()"Require Coq.Vectors.Vector.\nRequire Import Coq.Strings.String Coq.Arith.PeanoNat.\nImport EqNotations Vector.VectorNotations."))
+("query0"("Add"()"Require Stdlib.Vectors.Vector.\nRequire Import Stdlib.Strings.String Stdlib.Arith.PeanoNat.\nImport EqNotations Vector.VectorNotations."))
 ("query1"("Exec""2"))
 ("query2"("Query"(("sid""2"))"EGoals"))
 ("query3"("Exec""3"))