From 4bcf97e8e3f31b52e4ec14d0eefe6e755d5dd087 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 19 Jul 2024 18:28:23 +0200 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19310 --- serapi/serapi_protocol.ml | 4 ++-- sertop/comp_common.ml | 2 +- sertop/sertop_arg.ml | 2 +- sertop/sertop_sexp.ml | 2 +- tests/genarg/extraction.v | 2 +- tests/genarg/libTactics.v | 14 +++++++------- tests/sername/nat_add.out | 4 ++-- tests/sertop/full_env.in | 2 +- 8 files changed, 16 insertions(+), 16 deletions(-) diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml index 1e9b8eff..29493fc0 100644 --- 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 index 0fc709be..a722446d 100644 --- 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 index 671ba6fe..a87e0fc9 100644 --- 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 index 02cfa7f0..11546c37 100644 --- 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 index ec92c845..a771e714 100644 --- 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 index 451a77ad..5f895f69 100644 --- 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 index 205d108f..d127ebcf 100644 --- 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 index 6cf9c6e1..5cab0a4b 100644 --- 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"))