Adapt to https://github.com/coq/coq/pull/19530

lf-current/Extraction.v

@@ -10,15 +10,15 @@
     OCaml (the most mature), Haskell (mostly works), and Scheme (a bit
     out of date). *)
 
-Require Coq.extraction.Extraction.
+From Coq Require Extraction.
 Extraction Language OCaml.
 
 (** Now we load up the Coq environment with some definitions, either
     directly or by importing them from other modules. *)
 
-From Coq Require Import Arith.Arith.
+From Coq Require Import Arith.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.EqNat.
+From Coq Require Import EqNat.
 From LF Require Import ImpCEvalFun.
 
 (** Finally, we tell Coq the name of a definition to extract and the

lf-current/Imp.v

@@ -22,12 +22,12 @@
     reasoning about imperative programs. *)
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
-From Coq Require Import Bool.Bool.
+From Coq Require Import Bool.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.EqNat. Import Nat.
+From Coq Require Import Arith.
+From Coq Require Import EqNat. Import Nat.
 From Coq Require Import Lia.
-From Coq Require Import Lists.List. Import ListNotations.
+From Coq Require Import List. Import ListNotations.
 From Coq Require Import Strings.String.
 From LF Require Import Maps.
 Set Default Goal Selector "!".

lf-current/ImpCEvalFun.v

@@ -11,10 +11,10 @@
 (** * A Broken Evaluator *)
 
 From Coq Require Import Lia.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.PeanoNat.
+From Coq Require Import Arith.
+From Coq Require Import PeanoNat.
 Import Nat.
-From Coq Require Import Arith.EqNat.
+From Coq Require Import EqNat.
 From LF Require Import Imp Maps.
 
 (** Here was our first try at an evaluation function for commands,

lf-current/ImpParser.v

@@ -20,10 +20,10 @@
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 From Coq Require Import Strings.String.
 From Coq Require Import Strings.Ascii.
-From Coq Require Import Arith.Arith.
+From Coq Require Import Arith.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.EqNat.
-From Coq Require Import Lists.List. Import ListNotations.
+From Coq Require Import EqNat.
+From Coq Require Import List. Import ListNotations.
 From LF Require Import Maps Imp.
 
 (* ################################################################# *)

lf-current/Maps.v

@@ -29,11 +29,11 @@
     own definitions and theorems the same as their counterparts in the
     standard library, wherever they overlap. *)
 
-From Coq Require Import Arith.Arith.
-From Coq Require Import Bool.Bool.
-Require Export Coq.Strings.String.
-From Coq Require Import Logic.FunctionalExtensionality.
-From Coq Require Import Lists.List.
+From Coq Require Import Arith.
+From Coq Require Import Bool.
+From Coq Require Export String.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import List.
 Import ListNotations.
 Set Default Goal Selector "!".
 

lf-current/imp.ml

@@ -12,12 +12,9 @@ let rec app l m =
   | [] -> m
   | a :: l1 -> a :: (app l1 m)
 
-module Coq__1 = struct
- (** val add : int -> int -> int **)
+(** val add : int -> int -> int **)
 
- let rec add = ( + )
-end
-include Coq__1
+let rec add = ( + )
 
 (** val mul : int -> int -> int **)
 
@@ -133,6 +130,22 @@ type n =
 | Npos of positive
 
 module Pos =
+ struct
+  (** val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 **)
+
+  let rec iter_op op p a =
+    match p with
+    | XI p0 -> op a (iter_op op p0 (op a a))
+    | XO p0 -> iter_op op p0 (op a a)
+    | XH -> a
+
+  (** val to_nat : positive -> int **)
+
+  let to_nat x =
+    iter_op add x ((fun x -> x + 1) 0)
+ end
+
+module Coq_Pos =
  struct
   (** val succ : positive -> positive **)
 
@@ -187,19 +200,6 @@ module Pos =
     | XI p -> add y (XO (mul p y))
     | XO p -> XO (mul p y)
     | XH -> y
-
-  (** val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 **)
-
-  let rec iter_op op p a =
-    match p with
-    | XI p0 -> op a (iter_op op p0 (op a a))
-    | XO p0 -> iter_op op p0 (op a a)
-    | XH -> a
-
-  (** val to_nat : positive -> int **)
-
-  let to_nat x =
-    iter_op Coq__1.add x ((fun x -> x + 1) 0)
  end
 
 module N =
@@ -211,7 +211,7 @@ module N =
     | N0 -> m
     | Npos p -> (match m with
                  | N0 -> n0
-                 | Npos q -> Npos (Pos.add p q))
+                 | Npos q -> Npos (Coq_Pos.add p q))
 
   (** val mul : n -> n -> n **)
 
@@ -220,7 +220,7 @@ module N =
     | N0 -> N0
     | Npos p -> (match m with
                  | N0 -> N0
-                 | Npos q -> Npos (Pos.mul p q))
+                 | Npos q -> Npos (Coq_Pos.mul p q))
 
   (** val to_nat : n -> int **)
 
@@ -229,18 +229,18 @@ module N =
   | Npos p -> Pos.to_nat p
  end
 
-(** val rev : 'a1 list -> 'a1 list **)
-
-let rec rev = function
-| [] -> []
-| x :: l' -> app (rev l') (x :: [])
-
 (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
 
 let rec map f = function
 | [] -> []
 | a :: t -> (f a) :: (map f t)
 
+(** val rev : 'a1 list -> 'a1 list **)
+
+let rec rev = function
+| [] -> []
+| x :: l' -> app (rev l') (x :: [])
+
 (** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1 **)
 
 let rec fold_left f l a0 =

lf-current/imp.mli

@@ -36,6 +36,13 @@ type n =
 | Npos of positive
 
 module Pos :
+ sig
+  val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1
+
+  val to_nat : positive -> int
+ end
+
+module Coq_Pos :
  sig
   val succ : positive -> positive
 
@@ -44,10 +51,6 @@ module Pos :
   val add_carry : positive -> positive -> positive
 
   val mul : positive -> positive -> positive
-
-  val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1
-
-  val to_nat : positive -> int
  end
 
 module N :
@@ -59,10 +62,10 @@ module N :
   val to_nat : n -> int
  end
 
-val rev : 'a1 list -> 'a1 list
-
 val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
 
+val rev : 'a1 list -> 'a1 list
+
 val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1
 
 val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1

plf-current/Equiv.v

@@ -2,14 +2,14 @@
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 From PLF Require Import Maps.
-From Coq Require Import Bool.Bool.
-From Coq Require Import Arith.Arith.
+From Coq Require Import Bool.
+From Coq Require Import Arith.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.PeanoNat. Import Nat.
-From Coq Require Import Arith.EqNat.
+From Coq Require Import PeanoNat. Import Nat.
+From Coq Require Import EqNat.
 From Coq Require Import Lia.
-From Coq Require Import Lists.List. Import ListNotations.
-From Coq Require Import Logic.FunctionalExtensionality.
+From Coq Require Import List. Import ListNotations.
+From Coq Require Import FunctionalExtensionality.
 From PLF Require Export Imp.
 Set Default Goal Selector "!".
 

plf-current/Hoare.v

@@ -2,10 +2,10 @@
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 From PLF Require Import Maps.
-From Coq Require Import Bool.Bool.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.EqNat.
-From Coq Require Import Arith.PeanoNat. Import Nat.
+From Coq Require Import Bool.
+From Coq Require Import Arith.
+From Coq Require Import EqNat.
+From Coq Require Import PeanoNat. Import Nat.
 From Coq Require Import Lia.
 From PLF Require Export Imp.
 Set Default Goal Selector "!".

plf-current/Hoare2.v

@@ -4,10 +4,10 @@ Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 Set Warnings "-intuition-auto-with-star".
 From Coq Require Import Strings.String.
 From PLF Require Import Maps.
-From Coq Require Import Bool.Bool.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.EqNat.
-From Coq Require Import Arith.PeanoNat. Import Nat.
+From Coq Require Import Bool.
+From Coq Require Import Arith.
+From Coq Require Import EqNat.
+From Coq Require Import PeanoNat. Import Nat.
 From Coq Require Import Lia.
 From PLF Require Export Imp.
 From PLF Require Import Hoare.

plf-current/Imp.v

@@ -22,12 +22,12 @@
     reasoning about imperative programs. *)
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
-From Coq Require Import Bool.Bool.
+From Coq Require Import Bool.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.EqNat. Import Nat.
+From Coq Require Import Arith.
+From Coq Require Import EqNat. Import Nat.
 From Coq Require Import Lia.
-From Coq Require Import Lists.List. Import ListNotations.
+From Coq Require Import List. Import ListNotations.
 From Coq Require Import Strings.String.
 From PLF Require Import Maps.
 Set Default Goal Selector "!".

plf-current/LibTactics.v

@@ -368,7 +368,7 @@ Ltac fast_rm_inside E :=
     Note: the tactic [number_to_nat] is extended in [LibInt] to
     take into account the [Z] type. *)
 
-Require Coq.Numbers.BinNums Coq.ZArith.BinInt.
+From Coq Require BinNums BinInt.
 
 Definition ltac_int_to_nat (x:BinInt.Z) : nat :=
   match x with
@@ -2536,7 +2536,7 @@ Tactic Notation "subst_eq" constr(E) :=
 (* ================================================================= *)
 (** ** Tactics to Work with Proof Irrelevance *)
 
-Require Import Coq.Logic.ProofIrrelevance.
+From Coq Require Import ProofIrrelevance.
 
 (** [pi_rewrite E] replaces [E] of type [Prop] with a fresh
     unification variable, and is thus a practical way to
@@ -3138,7 +3138,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.
+From Coq.Program Require Import Equality.
 
 Ltac inductions_post :=
   unfold eq' in *.
@@ -3215,8 +3215,8 @@ Tactic Notation "induction_wf" ident(IH) ":" 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 Coq.micromega.Lia.
+From Coq Require Import Compare_dec.
+From Coq Require Import Lia.
 
 Lemma induct_height_max2 : forall n1 n2 : nat,
   exists n, n1 < n /\ n2 < n.

plf-current/Maps.v

@@ -29,11 +29,11 @@
     own definitions and theorems the same as their counterparts in the
     standard library, wherever they overlap. *)
 
-From Coq Require Import Arith.Arith.
-From Coq Require Import Bool.Bool.
+From Coq Require Import Arith.
+From Coq Require Import Bool.
 Require Export Coq.Strings.String.
-From Coq Require Import Logic.FunctionalExtensionality.
-From Coq Require Import Lists.List.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import List.
 Import ListNotations.
 Set Default Goal Selector "!".
 

plf-current/Norm.v

@@ -1,7 +1,7 @@
 (** * Norm: Normalization of STLC *)
 
 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
-From Coq Require Import Lists.List.
+From Coq Require Import List.
 From Coq Require Import Strings.String.
 From PLF Require Import Maps.
 From PLF Require Import Smallstep.

plf-current/PE.v

@@ -35,13 +35,13 @@
     without knowing the initial value of [Y]. *)
 
 From PLF Require Import Maps.
-From Coq Require Import Bool.Bool.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.EqNat.
-From Coq Require Import Arith.PeanoNat. Import Nat.
+From Coq Require Import Bool.
+From Coq Require Import Arith.
+From Coq Require Import EqNat.
+From Coq Require Import PeanoNat. Import Nat.
 From Coq Require Import Lia.
-From Coq Require Import Logic.FunctionalExtensionality.
-From Coq Require Import Lists.List.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import List.
 Import ListNotations.
 
 From PLF Require Import Smallstep.

plf-current/References.v

@@ -33,12 +33,12 @@ Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
 Set Warnings "-deprecated-syntactic-definition".
 From Coq Require Import Strings.String.
 From Coq Require Import Init.Nat.
-From Coq Require Import Arith.Arith.
-From Coq Require Import Arith.PeanoNat.
+From Coq Require Import Arith.
+From Coq Require Import PeanoNat.
 From Coq Require Import Lia.
 From PLF Require Import Maps.
 From PLF Require Import Smallstep.
-From Coq Require Import Lists.List. Import Datatypes.
+From Coq Require Import List. Import Datatypes.
 Check length.
 
 Import Nat.