Adapt to rocq-prover/rocq#21851

Author: proux01

apps/derive/elpi/bcongr.elpi

@@ -20,7 +20,7 @@ func bo-args term, term, term, list arg -> term.
 bo-args (prod N S T) K1 K2 Hs (fun `x` S x\ fun `y` S y\ fun `b` {{bool}} b\ R x y b) :- !,
   @pi-decl `x` S x\
   @pi-decl `y` S y\
-  @pi-decl `b` {{ Coq.Init.Datatypes.bool }} b\
+  @pi-decl `b` {{ Corelib.Init.Datatypes.bool }} b\
   @pi-decl Hn (TH x y b) h\
   do! [
     TH x y b = {{ lib:elpi.reflect (lib:@elpi.eq lp:S lp:x lp:y) lp:b }},

apps/derive/tests-stdlib/test_derive.v

@@ -67,7 +67,7 @@ Redirect "tmp" Check list_eqb_correct.
 Redirect "tmp" Check list_eqb_refl.
 (* ---------------------------------------------------- *)
 
-Require Vector.
+From Stdlib Require Vector.
 Elpi Print derive "elpi.apps.derive.tests/derive".
 #[only(eqOK), verbose] derive nat.
 Module Vector.

apps/derive/theories/derive/eq.v

@@ -12,8 +12,8 @@ From elpi.apps Require Import derive.
 From Corelib Require Import PrimInt63 PrimFloat.
 From elpi.apps.derive Require Import PrimStringEqb.
 
-Register Coq.Numbers.Cyclic.Int63.PrimInt63.eqb as elpi.derive.eq_unit63.
-Register Coq.Floats.PrimFloat.eqb as elpi.derive.eq_float64.
+Register Corelib.Numbers.Cyclic.Int63.PrimInt63.eqb as elpi.derive.eq_unit63.
+Register Corelib.Floats.PrimFloat.eqb as elpi.derive.eq_float64.
 
 Elpi Db derive.eq.db lp:{{
 

apps/eltac/tests-stdlib/test_injection.v

@@ -12,8 +12,9 @@ intro E.
 assumption.
 Qed.
 
-Require Vector.
-Require Import ssreflect Arith.
+From Stdlib Require Vector.
+From Corelib Require Import ssreflect.
+From Stdlib Require Import Arith.
 
 Elpi derive.projK Vector.t.
 
@@ -28,4 +29,4 @@ split.
   exact Eab.
 rewrite -[v2](projT2_eq Esigv12) /=.
 by rewrite (UIP_nat _ _ (projT1_eq Esigv12) (eq_refl n)).
-Qed.
+Qed.

apps/tc/tests-stdlib/bigTest.v

@@ -7,10 +7,10 @@ abstract interfaces for ordered structures, sets, and various other data
 structures. *)
 
 (* We want to ensure that [le] and [lt] refer to operations on [nat].
-These two functions being defined both in [Coq.Bool] and in [Coq.Peano],
-we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
-(* We also want to ensure that notations from [Coq.Utf8] take precedence
-over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
+These two functions being defined both in [Stdlib.Bool] and in [Stdlib.Peano],
+we must export [Stdlib.Peano] later than any export of [Stdlib.Bool]. *)
+(* We also want to ensure that notations from [Stdlib.Utf8] take precedence
+over the ones of [Stdlib.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
 From Corelib Require Export Morphisms RelationClasses ListDef Setoid.
 From Stdlib Require Export Bool List Peano Utf8 Permutation.
 From Stdlib Require Export Program.Basics Program.Syntax.

apps/tc/tests-stdlib/eqSimplDef.v

@@ -1,4 +1,4 @@
-Require Import Bool Arith List.
+From Stdlib Require Import Bool Arith List.
 
 Class Eqb A : Type := eqb : A -> A -> bool.
 Global Hint Mode Eqb + : typeclass_instances.
@@ -7,5 +7,5 @@ Notation " x == y " := (eqb x y) (no associativity, at level 70).
 
 Global Instance eqU : Eqb unit := { eqb x y := true }.
 Global Instance eqB : Eqb bool := { eqb x y := if x then y else negb y }.
-Global Instance eqP {A B} `{Eqb A} `{Eqb B} : Eqb (A * B) := { 
-  eqb x y := (fst x == fst y) && (snd x == snd y) }.
+Global Instance eqP {A B} `{Eqb A} `{Eqb B} : Eqb (A * B) := {
+  eqb x y := (fst x == fst y) && (snd x == snd y) }.

builtin-doc/coq-builtin.elpi

@@ -1676,7 +1676,7 @@ external func coq.ltac.collect-simple-goals term -> list goal,
 % Note that each TACTIC EXTEND block can have many entries and their
 % numbering
 % starts from 0. Also, each block has a name, "Lia" in this case.
-%     
+% 
 % When the diagnostic is (error Msg), then GL is not set.
 % 
 % Supported attributes:

examples-stdlib/example_open_terms.v

@@ -1,5 +1,5 @@
 From elpi Require Import elpi.
-Require Import Arith ZArith List FunctionalExtensionality.
+From Stdlib Require Import Arith ZArith List FunctionalExtensionality.
 
 Axiom map2 : (nat -> nat -> nat) -> list nat -> list nat -> list nat.
 

examples-stdlib/example_reflexive_tactic.v

@@ -10,7 +10,7 @@
 *)
 
 From elpi Require elpi.
-Require Arith ZArith Psatz List ssreflect.
+From Stdlib Require Arith ZArith Psatz List ssreflect.
 
 Import elpi.
 Import Arith ZArith Psatz List ssreflect.

examples/tutorial_coq_elpi_HOAS.v

@@ -416,8 +416,8 @@ of constants.
 
 |*)
 
-Register Coq.Init.Datatypes.nat as my.N.
-Register Coq.Init.Logic.eq as my.eq.
+Register Corelib.Init.Datatypes.nat as my.N.
+Register Corelib.Init.Logic.eq as my.eq.
 
 Elpi Query lp:{{