Merge pull request Mtac2#428 from proux01/rocq21851

Adapt to rocq-prover/rocq#21851

Author: Janno

examples/basics_tutorial.v

@@ -47,9 +47,7 @@ Import M.notations.
 (** In addition, we import a couple of modules from the standard
 library that we are going to use in some examples. *)
 
-Require Import Arith.Arith.
-Require Import Lists.List.
-Require Import Strings.String.
+From Stdlib Require Import Arith List String.
 
 Set Implicit Arguments.
 Notation "x == y" := (Nat.eqb x y) (at level 60).

examples/tactics.v

@@ -21,7 +21,7 @@ Require Import Mtac2.Mtac2.
 Import T.
 
 (** We're going to prove stuff about lists. *)
-Require Import Lists.List.
+From Stdlib Require Import List.
 Import Lists.List.ListNotations.
 
 (** A simple example to warm up. *)

examples/tauto.v

@@ -1,5 +1,5 @@
 From Mtac2 Require Import Mtac2 Ttactics Sorts.
-From Coq Require Import List.
+From Stdlib Require Import List.
 Import M.notations.
 Import M.
 Import ListNotations.

src/constrs.ml

@@ -218,9 +218,9 @@ end
 module CoqPositive = struct
   open Constrs
 
-  let xI = mkGlobal "Coq.Numbers.BinNums.xI"
-  let xO = mkGlobal "Coq.Numbers.BinNums.xO"
-  let xH = mkGlobal "Coq.Numbers.BinNums.xH"
+  let xI = mkGlobal "Corelib.Numbers.BinNums.xI"
+  let xO = mkGlobal "Corelib.Numbers.BinNums.xO"
+  let xH = mkGlobal "Corelib.Numbers.BinNums.xH"
 
   let isH env sigma = isGlobal env sigma xH
   let isI env sigma = isGlobal env sigma xI
@@ -255,9 +255,9 @@ end
 
 module CoqN = struct
   open Constrs
-  (* let tN = Constr.mkConstr "Coq.Numbers.BinNums.N" *)
-  let h0 = mkGlobal "Coq.Numbers.BinNums.N0"
-  let hP = mkGlobal "Coq.Numbers.BinNums.Npos"
+  (* let tN = Constr.mkConstr "Corelib.Numbers.BinNums.N" *)
+  let h0 = mkGlobal "Corelib.Numbers.BinNums.N0"
+  let hP = mkGlobal "Corelib.Numbers.BinNums.Npos"
 
   let is0 env sigma = isGlobal env sigma h0
   let isP env sigma = isGlobal env sigma hP
@@ -290,9 +290,9 @@ end
 module CoqZ = struct
   open Constrs
 
-  let z0 =   mkGlobal "Coq.Numbers.BinNums.Z0"
-  let zpos = mkGlobal "Coq.Numbers.BinNums.Zpos"
-  let zneg = mkGlobal "Coq.Numbers.BinNums.Zneg"
+  let z0 =   mkGlobal "Corelib.Numbers.BinNums.Z0"
+  let zpos = mkGlobal "Corelib.Numbers.BinNums.Zpos"
+  let zneg = mkGlobal "Corelib.Numbers.BinNums.Zneg"
 
   let to_coq n =
     if n = 0 then
@@ -306,9 +306,9 @@ end
 module CoqBool = struct
   open ConstrBuilder
 
-  let boolBuilder = from_string "Coq.Init.Datatypes.bool"
-  let trueBuilder = from_string "Coq.Init.Datatypes.true"
-  let falseBuilder = from_string "Coq.Init.Datatypes.false"
+  let boolBuilder = from_string "Corelib.Init.Datatypes.bool"
+  let trueBuilder = from_string "Corelib.Init.Datatypes.true"
+  let falseBuilder = from_string "Corelib.Init.Datatypes.false"
 
   let mkType = build boolBuilder
   let mkTrue = build trueBuilder
@@ -326,7 +326,7 @@ end
 module CoqAscii = struct
   open ConstrBuilder
 
-  let asciiBuilder = from_string "Coq.Strings.Ascii.Ascii"
+  let asciiBuilder = from_string "Stdlib.Strings.Ascii.Ascii"
 
   let from_coq (env, sigma) c =
     let (h, args) = decompose_appvect sigma c in
@@ -347,8 +347,8 @@ end
 module CoqString = struct
   open ConstrBuilder
 
-  let emptyBuilder = from_string "Coq.Strings.String.EmptyString"
-  let stringBuilder = from_string "Coq.Strings.String.String"
+  let emptyBuilder = from_string "Stdlib.Strings.String.EmptyString"
+  let stringBuilder = from_string "Stdlib.Strings.String.String"
 
   exception NotAString
 
@@ -383,8 +383,8 @@ end
 module CoqUnit = struct
   open ConstrBuilder
 
-  let unitBuilder = from_string "Coq.Init.Datatypes.unit"
-  let ttBuilder = from_string "Coq.Init.Datatypes.tt"
+  let unitBuilder = from_string "Corelib.Init.Datatypes.unit"
+  let ttBuilder = from_string "Corelib.Init.Datatypes.tt"
 
   let mkType = build unitBuilder
   let mkTT = build ttBuilder

tests/ConstrSelector.v

@@ -34,8 +34,7 @@ MProof.
   select (_ = _) >>= rrewrite ;; reflexivity.
 Qed.
 
-Require Import Coq.Arith.Arith.
-Require Import Coq.Arith.EqNat.
+From Stdlib Require Import Arith EqNat.
 
 Inductive id : Type :=
   | Id : nat -> id.
@@ -147,7 +146,7 @@ Inductive ceval : com -> state -> state -> Prop :=
 
   where "c1 '/' st '\\' st'" := (ceval c1 st st').
 
-Require Import Strings.String.
+From Stdlib Require Import String.
 
 Definition remember {A} (x:A) (def eq : string) : tactic :=
   cpose_base (TheName def) x (fun y:A=>

tests/DepDestruct.v

@@ -193,18 +193,18 @@ Abort.
 End ExampleReflect.
 
 Set Unicoq Try Solving Eqn.
-Require Vector.
+From Stdlib Require Vector.
 Module VectorExample.
 Import Vector.
-Goal forall n (v : t nat n), n = Coq.Lists.List.length (to_list v).
+Goal forall n (v : t nat n), n = Stdlib.Lists.List.length (to_list v).
 Proof.
   pose (it := iTele (fun n => @iBase (Typeₛ) (t nat n))).
   pose (vnil := ((@cBase Typeₛ it (aTele 0 aBase) (nil nat))) : CTele it).
   pose (vcons := (cProd (fun a => cProd (fun n => cProd (fun (v : t nat n) => (@cBase Typeₛ it (aTele (S n) aBase) (cons _ a _ v)))))) : CTele it).
   fix f 2.
   intros n v.
   pose (a := (aTele n (aBase)) : ATele it).
-  pose (rt := M.eval (abstract_goal (rsort := Propₛ) (n = Coq.Lists.List.length (to_list v)) a v)).
+  pose (rt := M.eval (abstract_goal (rsort := Propₛ) (n = Stdlib.Lists.List.length (to_list v)) a v)).
   simpl in vcons.
   cbn beta iota zeta delta -[RTele] in rt.
   assert (N : branch_of_CTele rt vnil).

tests/Exhaustive.v

@@ -1,4 +1,4 @@
-Require Import Strings.String.
+From Stdlib Require Import String.
 From Mtac2 Require Import Base List Exhaustive.
 Import M.notations.
 

tests/UnivSanityCheck.v

@@ -4,8 +4,8 @@ Import M.notations.
 
 Print Universes "universes-mtac2.txt".
 Import M.
-Require Import Coq.Numbers.BinNums.
-Require Import Strings.String.
+From Corelib Require Import BinNums.
+From Stdlib Require Import String.
 
 Definition file := "universes-mtac2.txt".
 Definition magic_number := "0".

tests/abs.v

@@ -1,9 +1,9 @@
 From Mtac2
 Require Export Mtac2.
 
-Require Import Strings.String.
+From Stdlib Require Import String.
 
-Require Import Lists.List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 Definition assert_eq {A} (a b : A) : M True := mmatch b with a => M.ret I | _ => M.raise exception end.

tests/bugs.v

@@ -1,6 +1,6 @@
 From Mtac2 Require Import Logic Datatypes Mtac2.
 
-Require Import Bool.Bool.
+From Stdlib Require Import Bool.
 Import T.
 
 (** A bug with destruct *)