diff --git a/theories/additions/AM.v b/theories/additions/AM.v
index d5139a0b..52ef9818 100644
--- a/theories/additions/AM.v
+++ b/theories/additions/AM.v
@@ -4,16 +4,19 @@
 (** Work in progress 
 
 *)
-
-Require Import Monoid_def Monoid_instances List PArith Relations.
-Require Import Strategies Lia.
-Generalizable All Variables.
+From Coq Require Import List PArith Relations Lia.
 Import Morphisms.
+
+From additions Require Import Monoid_def Monoid_instances Strategies.
 Import Monoid_def.
-Require Import Recdef Wf_nat.
-Require Import More_on_positive.
-Require  Import Pow.
-Require Import Euclidean_Chains.
+
+From Coq Require Import Recdef Wf_nat.
+From additions Require Import More_on_positive Pow  Euclidean_Chains
+  Dichotomy BinaryStrat.
+Generalizable All Variables.
+
+
+
 
 (** basic instructions *)
 (* begin snippet AMDef *)
@@ -137,7 +140,7 @@ Compute chain_apply C31_7 Natplus 1%nat.
 
 (* end snippet AMSemb *)
 
-Require Import NArith.
+From Coq Require Import NArith.
 
 Compute chain_apply C31_7 NMult 2%N.
 
@@ -522,8 +525,6 @@ Section CompositionProofs.
 
 (** *  Euclidean chain generation *)
 
-Require Import Dichotomy BinaryStrat.
-
 Definition  OK (s: signature) 
   := fun c: code => correctness_statement s c.
 
diff --git a/theories/additions/Addition_Chains.v b/theories/additions/Addition_Chains.v
index 4598c599..fe1db714 100644
--- a/theories/additions/Addition_Chains.v
+++ b/theories/additions/Addition_Chains.v
@@ -4,12 +4,11 @@ Pierre Casteran, LaBRI, University of Bordeaux
 
 *)
 
-Require Export Monoid_instances Pow Lia List.
-Require Import Relations RelationClasses.
-
+From additions Require Export Monoid_instances Pow.
+From Coq Require Import Relations RelationClasses Lia List.
 From Param Require Import Param.
  
-Require Import More_on_positive.
+From additions Require Import More_on_positive.
 Generalizable Variables A op one Aeq.
 Infix "==" := Monoid_def.equiv (at level 70) : type_scope.
 Open Scope nat_scope.
diff --git a/theories/additions/BinaryStrat.v b/theories/additions/BinaryStrat.v
index cf514f91..88350ab2 100644
--- a/theories/additions/BinaryStrat.v
+++ b/theories/additions/BinaryStrat.v
@@ -6,8 +6,9 @@
 *)
  
 
-Require Import Arith NArith Pow Compatibility More_on_positive Lia.
-Require Export Strategies.
+From Coq Require Import Arith NArith Lia.
+From additions Require Import  Pow Compatibility More_on_positive.
+From additions Require Export Strategies.
 
 Open Scope positive_scope.
 
diff --git a/theories/additions/Compatibility.v b/theories/additions/Compatibility.v
index 19feb4e9..dccbc613 100644
--- a/theories/additions/Compatibility.v
+++ b/theories/additions/Compatibility.v
@@ -7,9 +7,9 @@ equivalence theorems with functions defined in our module [Pow].
 
  *)
 
-Require Import Monoid_def Lia Monoid_instances
-     ArithRing  Pow.
-
+From additions Require Import Monoid_def Monoid_instances
+       Pow.
+From Coq Require Import Lia ArithRing.
 
 (** ** really logarithmic versions of N.pow, Pos.pow and Z.pow 
  
diff --git a/theories/additions/Demo.v b/theories/additions/Demo.v
index 13b1a8bc..84d01e26 100644
--- a/theories/additions/Demo.v
+++ b/theories/additions/Demo.v
@@ -4,9 +4,7 @@ Module Alt.
 
 End Alt.
 
-Require Import Arith Lia.
-
-Require Import Even.
+From Coq Require Import Arith Lia Even.
 
 Lemma alt_double_ok n : Nat.double n = Alt.double n.
 Proof.
diff --git a/theories/additions/Demo_power.v b/theories/additions/Demo_power.v
index 3a1a8053..f626ab98 100644
--- a/theories/additions/Demo_power.v
+++ b/theories/additions/Demo_power.v
@@ -1,6 +1,4 @@
-Require Import Monoid_def 
-               Monoid_instances
-               Pow.
+From additions Require Import Monoid_def Monoid_instances Pow.
 (* begin snippet DemoPower *)
 Open Scope M_scope.
 
diff --git a/theories/additions/Dichotomy.v b/theories/additions/Dichotomy.v
index 52b7c548..42d74a58 100644
--- a/theories/additions/Dichotomy.v
+++ b/theories/additions/Dichotomy.v
@@ -9,8 +9,9 @@
 *)
  
 
-Require Import Arith NArith Pow Compatibility More_on_positive.
-Require Export Strategies.
+From Coq Require Import Arith NArith.
+From additions Require Export Strategies Pow Compatibility 
+  More_on_positive.
 
 Open Scope positive_scope.
 
@@ -170,8 +171,7 @@ Proof.
 intros p H; unfold dicho; generalize (dicho_aux_lt p H).
 intro H0; assert (2 <= N.pos p / (N.pos (dicho_aux p)) )%N.
 - replace 2%N with (2%N * Npos (dicho_aux p) / Npos (dicho_aux p))%N.
-  + apply N.div_le_mono.
-    * discriminate.
+  + apply (* N.Div0.div_le_mono. *) N.div_le_mono; try discriminate. 
     * replace 2%N with (Npos 2%positive); cbn;auto.
   + rewrite N.div_mul; [auto | discriminate].
 - case_eq (N.pos p / N.pos (dicho_aux p))%N.
diff --git a/theories/additions/Euclidean_Chains.v b/theories/additions/Euclidean_Chains.v
index 687ac45a..a28ff77b 100644
--- a/theories/additions/Euclidean_Chains.v
+++ b/theories/additions/Euclidean_Chains.v
@@ -14,13 +14,12 @@ small computation may be parameterized by the context in which it will be
 
 
 
-Require Import Inverse_Image  Inclusion  Wf_nat.
-Require Import Addition_Chains  NArith  Arith PArith  Compatibility.  
-Require Import More_on_positive.
-Import Monoid_def  Pow.
-Require Import Recdef Wf_nat.
-Require Import  More_on_positive .
-Require Import Wf_transparent Lexicographic_Product  Dichotomy BinaryStrat.
+From Coq Require Import Inverse_Image  Inclusion  Wf_nat 
+  NArith  Arith PArith Recdef Wf_nat Lexicographic_Product Lia.
+From additions Require Import Addition_Chains    Compatibility 
+  More_on_positive Wf_transparent   Dichotomy BinaryStrat.
+From Coq Require Import Lia.
+
 Generalizable All Variables.
 Import Morphisms.
 Import Monoid_def.
@@ -1538,7 +1537,7 @@ Arguments big_chain _%type_scope.
 Remark RM : (1 < 56789)%N. 
 Proof. reflexivity. Qed.
 
-Definition M := Nmod_Monoid _ RM.
+Definition M := Nmod_Monoid  _ RM.
 
 Definition exp56789 x := chain_apply big_chain (M:=M) x.
 
diff --git a/theories/additions/Fib2.v b/theories/additions/Fib2.v
index 85a4d711..b36c72d1 100644
--- a/theories/additions/Fib2.v
+++ b/theories/additions/Fib2.v
@@ -1,6 +1,8 @@
 
 
-Require Import NArith Ring Monoid_instances Euclidean_Chains Pow
+From Coq Require Import NArith Ring.
+
+From additions Require Import Monoid_instances Euclidean_Chains Pow
         Strategies Dichotomy BinaryStrat.
 Import Addition_Chains. 
 Open Scope N_scope.
@@ -135,7 +137,8 @@ Time Compute fib_eucl half 153.
 Finished transaction in 0.002 secs (0.002u,0.s) (successful)
 *)
 
-Require Import AM.
+From additions Require Import AM.
+
 Definition fib_with_chain c :=
   match chain_apply c  Mul2 (1,0) with
     Some ((a,b), nil) => Some (a+b) | _ => None end.
diff --git a/theories/additions/FirstSteps.v b/theories/additions/FirstSteps.v
index cc62ed77..dad0f1c4 100644
--- a/theories/additions/FirstSteps.v
+++ b/theories/additions/FirstSteps.v
@@ -1,7 +1,6 @@
 (** Polymorphic versions of exponentiation functions *)
 
-Require Import Arith ZArith.
-Require Import String.
+From Coq Require Import Arith ZArith String.
 
 (** 
   Polymorphic exponentiation functions 
diff --git a/theories/additions/Monoid_def.v b/theories/additions/Monoid_def.v
index 4ce00382..e5cc6e59 100644
--- a/theories/additions/Monoid_def.v
+++ b/theories/additions/Monoid_def.v
@@ -1,6 +1,4 @@
-Require Import RelationClasses.
-Require Import Relations Morphisms.
-Require Import String.
+From Coq Require Import RelationClasses Relations Morphisms String.
 
 Set Implicit Arguments.
 
diff --git a/theories/additions/More_on_positive.v b/theories/additions/More_on_positive.v
index 979f9204..e51b37c3 100644
--- a/theories/additions/More_on_positive.v
+++ b/theories/additions/More_on_positive.v
@@ -1,8 +1,8 @@
 
-Require Import Arith NArith Pow Compatibility Lia.
+From Coq Require Import Arith NArith  Lia Recdef.
+From additions Require Import Pow Compatibility Wf_transparent. 
 Open Scope positive_scope.
 Import Monoid_def.
-Require Import Recdef  Wf_transparent. 
 
 (** * Basic lemmas about positive and N *)
 
diff --git a/theories/additions/Trace_exercise.v b/theories/additions/Trace_exercise.v
index c71e5ac0..d4b487a4 100644
--- a/theories/additions/Trace_exercise.v
+++ b/theories/additions/Trace_exercise.v
@@ -1,7 +1,8 @@
 (* Trace of a chain *)
 (** Solution to an exercise *)
 
-
+From Coq Require Import List.
+Import ListNotations.
 Require Import Addition_Chains PArith.
 
 
diff --git a/theories/additions/Wf_transparent.v b/theories/additions/Wf_transparent.v
index 7d553d19..7384bf30 100644
--- a/theories/additions/Wf_transparent.v
+++ b/theories/additions/Wf_transparent.v
@@ -2,7 +2,7 @@
 *)
 
 
-Require Export Relation_Definitions.
+From Coq Require Export Relation_Definitions.
 
 Lemma wf_incl_transparent  :
 forall (A : Type) (R1 R2 : A -> A -> Prop),
diff --git a/theories/additions/fib.v b/theories/additions/fib.v
index a75a834a..bc66b996 100644
--- a/theories/additions/fib.v
+++ b/theories/additions/fib.v
@@ -1,8 +1,7 @@
 (** author Yves Bertot, Inria  *)
 
 
-Require Import Extraction.
-Require Import ZArith Lia.
+From Coq Require Import Extraction ZArith Lia.
 
 From mathcomp Require Import all_ssreflect all_algebra.
 
diff --git a/theories/gaia/GHessenberg.v b/theories/gaia/GHessenberg.v
index 3913e22a..414a44ad 100644
--- a/theories/gaia/GHessenberg.v
+++ b/theories/gaia/GHessenberg.v
@@ -6,8 +6,8 @@ From hydras Require Import DecPreOrder ON_Generic.
 From hydras Require Import T1 E0 Hessenberg.
 
 From gaia Require Export ssete9.
+From gaia_hydras Require Import T1Bridge. 
 
-Require Import T1Bridge. 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/gaia/GLarge_Sets.v b/theories/gaia/GLarge_Sets.v
index df3f7e9b..24480d0a 100644
--- a/theories/gaia/GLarge_Sets.v
+++ b/theories/gaia/GLarge_Sets.v
@@ -7,7 +7,7 @@
 From mathcomp Require Import all_ssreflect zify.
 From hydras Require Import T1.
 From hydras Require Import Canon Paths Large_Sets.
-Require Import T1Bridge GCanon GPaths.
+From gaia_hydras Require Import T1Bridge GCanon GPaths.
 
 From gaia Require Import ssete9.
 Import CantorOrdinal. 
diff --git a/theories/gaia/GPaths.v b/theories/gaia/GPaths.v
index e39db618..21d705e5 100644
--- a/theories/gaia/GPaths.v
+++ b/theories/gaia/GPaths.v
@@ -5,7 +5,7 @@
 
 From mathcomp Require Import all_ssreflect zify.
 From hydras Require Import Canon Paths.
-Require Import T1Bridge GCanon.
+From gaia_hydras Require Import T1Bridge GCanon.
 
 
 From hydras Require Import T1.
diff --git a/theories/gaia/GaiaToHydra.v b/theories/gaia/GaiaToHydra.v
index d2f4b78f..c617df1d 100644
--- a/theories/gaia/GaiaToHydra.v
+++ b/theories/gaia/GaiaToHydra.v
@@ -1,7 +1,7 @@
 (* begin snippet T1BridgeUse:: no-out *)
 
 From mathcomp Require Import all_ssreflect zify.
-Require Import T1Bridge . 
+From gaia_hydras Require Import T1Bridge . 
 From hydras Require Import T1. 
 
 From gaia Require Import ssete9.
diff --git a/theories/gaia/HydraGaia_Examples.v b/theories/gaia/HydraGaia_Examples.v
index 9d21eef3..3c2b7e5f 100644
--- a/theories/gaia/HydraGaia_Examples.v
+++ b/theories/gaia/HydraGaia_Examples.v
@@ -5,7 +5,8 @@ From hydras Require Import DecPreOrder ON_Generic.
 From hydras Require Import T1 E0 Hessenberg.
 From gaia Require Export ssete9.
 
-Require Import T1Bridge GCanon GHessenberg GLarge_Sets. 
+From gaia_hydras Require Import T1Bridge GCanon GHessenberg 
+  GLarge_Sets. 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
diff --git a/theories/gaia/T1Choice.v b/theories/gaia/T1Choice.v
index a03ac1da..71e02f4c 100644
--- a/theories/gaia/T1Choice.v
+++ b/theories/gaia/T1Choice.v
@@ -12,7 +12,7 @@ From mathcomp Require Import all_ssreflect zify.
 From Coq Require Import Logic.Eqdep_dec.
 From hydras Require Import DecPreOrder ON_Generic  T1 E0.
 From gaia Require Export ssete9.
-Require Import T1Bridge.
+From gaia_hydras Require Import T1Bridge.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/gaia/nfwfgaia.v b/theories/gaia/nfwfgaia.v
index a071b24d..d57c05bf 100644
--- a/theories/gaia/nfwfgaia.v
+++ b/theories/gaia/nfwfgaia.v
@@ -9,7 +9,7 @@
 
 
 From mathcomp
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+  Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import fintype bigop.
 
 Set Implicit Arguments.
diff --git a/theories/gaia/onType.v b/theories/gaia/onType.v
index cd288482..93710aad 100644
--- a/theories/gaia/onType.v
+++ b/theories/gaia/onType.v
@@ -205,7 +205,7 @@ Compute tricho om67 om12.
 
 (** To do :  Notation for epsilon0 *)
 
-Require Import T1Bridge.
+From gaia_hydras Require Import T1Bridge.
 
 Section ONEpsilon0Def. 
 
diff --git a/theories/goedel/PRrepresentable.v b/theories/goedel/PRrepresentable.v
index 43435722..b174758d 100644
--- a/theories/goedel/PRrepresentable.v
+++ b/theories/goedel/PRrepresentable.v
@@ -29,7 +29,7 @@ From hydras Require Export MoreLibHyps NewNotations.
 Import NNnotations. 
 #[local] Arguments apply _ _ _ : clear implicits.
 Import LispAbbreviations. 
-Require Import Utf8.
+From Coq Require Import Utf8.
 
 Coercion natToTerm : nat >-> Term.
 
diff --git a/theories/goedel/goedel2.v b/theories/goedel/goedel2.v
index 7ec3ea70..bbb38930 100644
--- a/theories/goedel/goedel2.v
+++ b/theories/goedel/goedel2.v
@@ -7,21 +7,15 @@ From hydras.Ackermann Require Import folReplace.
 From hydras.Ackermann Require Import folLogic3.
 From hydras.Ackermann Require Import subProp.
 From hydras.Ackermann Require Import ListExt.
-(*
-Require Import NNtheory.
-*)
+
 From Goedel Require Import fixPoint.
 From hydras.Ackermann Require Import NN2PA.
 From Goedel Require Import codeSysPrf.
 From hydras.Ackermann Require Import PAtheory.
 From hydras.Ackermann Require Import code.
-(*
-Require Import PRrepresentable.
-Require Import expressible.
-*)
 From hydras.Ackermann Require Import checkPrf.
 From hydras.Ackermann Require Import codeNatToTerm.
-Require Import rosserPA.
+From Goedel Require Import rosserPA.
 
 Section Goedel's_2nd_Incompleteness.
 
diff --git a/theories/ordinals/Ackermann/Deduction.v b/theories/ordinals/Ackermann/Deduction.v
index 068783c6..a984e3ad 100644
--- a/theories/ordinals/Ackermann/Deduction.v
+++ b/theories/ordinals/Ackermann/Deduction.v
@@ -6,8 +6,7 @@
 
 From Coq Require Import Ensembles List.
 
-Require Import folProof.
-Require Import folProp.
+From hydras.Ackermann Require Import folProof folProp.
 Import FolNotations.
 
 Section Deduction_Theorem.
diff --git a/theories/ordinals/Ackermann/LNN.v b/theories/ordinals/Ackermann/LNN.v
index 453fecc1..51376989 100644
--- a/theories/ordinals/Ackermann/LNN.v
+++ b/theories/ordinals/Ackermann/LNN.v
@@ -8,9 +8,10 @@ Original version by Russel O'Connor
 
 From Coq Require Import Arith Ensembles List.
 
-Require Export Languages folProof  folProp  folLogic3.
+From hydras.Ackermann Require Export Languages folProof  
+  folProp  folLogic3.
 From LibHyps Require Import LibHyps. 
-Require Import MoreLibHyps NewNotations.
+From hydras Require Import MoreLibHyps NewNotations.
 
 (** * Instantiations of a few generic constructs 
 
diff --git a/theories/ordinals/Ackermann/LNN2LNT.v b/theories/ordinals/Ackermann/LNN2LNT.v
index 9285ac22..d41d9ace 100644
--- a/theories/ordinals/Ackermann/LNN2LNT.v
+++ b/theories/ordinals/Ackermann/LNN2LNT.v
@@ -10,8 +10,9 @@
 (* begin hide *)
 From Coq Require Import Ensembles List Arith.
 
-Require Import misc ListExt folProp folProof Languages  subAll  subProp.
-Require Import folLogic3  folReplace LNN LNT  codeNatToTerm  NewNotations.
+From hydras.Ackermann 
+ Require Import misc ListExt folProp folProof Languages  subAll  
+ subProp  folLogic3  folReplace LNN LNT  codeNatToTerm  NewNotations.
 
 Import FolNotations  NNnotations.
 
diff --git a/theories/ordinals/Ackermann/LNT.v b/theories/ordinals/Ackermann/LNT.v
index 7991474f..41a637c5 100644
--- a/theories/ordinals/Ackermann/LNT.v
+++ b/theories/ordinals/Ackermann/LNT.v
@@ -7,7 +7,8 @@ Original version by Russel O'Connor
 
 From Coq Require Import Arith Ensembles List.
 
-Require Import Languages  folProof  folProp  folLogic3.
+From hydras.Ackermann 
+ Require Import Languages  folProof  folProp  folLogic3.
 
 (** * Instantiations of a few generic constructs 
 
diff --git a/theories/ordinals/Ackermann/Languages.v b/theories/ordinals/Ackermann/Languages.v
index 2ed3249c..146ff5b7 100644
--- a/theories/ordinals/Ackermann/Languages.v
+++ b/theories/ordinals/Ackermann/Languages.v
@@ -5,7 +5,7 @@
 (** TO do : reorganize Alectryon snippets *)
 
 From Coq Require Import Arith List.
-Require Import fol primRec code.
+From hydras.Ackermann Require Import fol primRec code.
 
 (**  * Language of Number Theory: [LNT] *)
 
diff --git a/theories/ordinals/Ackermann/ListExt.v b/theories/ordinals/Ackermann/ListExt.v
index cf56e5af..513e7999 100644
--- a/theories/ordinals/Ackermann/ListExt.v
+++ b/theories/ordinals/Ackermann/ListExt.v
@@ -6,7 +6,7 @@
    since it appears in many composed tactics. 
 *)
 
-Require Import Coq.Lists.List.
+From Coq Require Import Lists.List.
 
 Section List_Remove.
 
diff --git a/theories/ordinals/Ackermann/NN.v b/theories/ordinals/Ackermann/NN.v
index c60b097e..80ef82fd 100644
--- a/theories/ordinals/Ackermann/NN.v
+++ b/theories/ordinals/Ackermann/NN.v
@@ -9,8 +9,8 @@ Original version by Russel O'Connor
 
 From Coq Require Import Arith Lia  Ensembles List.
 
-Require Import folProp subAll  folLogic3 Languages.
-Require Export LNN.
+From hydras.Ackermann Require Import folProp subAll  folLogic3 Languages.
+From hydras.Ackermann Require Export LNN.
 From hydras Require Import Compat815 NewNotations.
 Import NNnotations. 
 (** * Axioms of [NN] *)
diff --git a/theories/ordinals/Ackermann/NN2PA.v b/theories/ordinals/Ackermann/NN2PA.v
index ed51af8b..450b5c38 100644
--- a/theories/ordinals/Ackermann/NN2PA.v
+++ b/theories/ordinals/Ackermann/NN2PA.v
@@ -7,10 +7,11 @@ Original version by Russel O'Connor
 
 From Coq Require Import Ensembles List Arith.
 
-Require Import folProp  folProof  subProp  folLogic3  folReplace  NN
+From hydras.Ackermann 
+  Require Import folProp  folProof  subProp  folLogic3  folReplace  NN
   PAtheory.
-Require Export LNN2LNT.
-Require Import subAll ListExt.
+From hydras.Ackermann Require Export LNN2LNT.
+From hydras.Ackermann Require Import subAll ListExt.
 Import NNnotations.
 
 Lemma NN2PA (f : fol.Formula LNN):
diff --git a/theories/ordinals/Ackermann/NNtheory.v b/theories/ordinals/Ackermann/NNtheory.v
index 241f1db2..f546cc98 100644
--- a/theories/ordinals/Ackermann/NNtheory.v
+++ b/theories/ordinals/Ackermann/NNtheory.v
@@ -1,9 +1,8 @@
 From Coq Require Import Arith Lia.
 
-Require Import folLogic3.
-Require Import folProp.
-Require Import subProp.
-Require Export NN.
+From hydras.Ackermann Require Import folLogic3 folProp subProp.
+From hydras.Ackermann Require Import folLogic3 folProp subProp. 
+From hydras.Ackermann Require Export NN.
 From hydras Require Import Compat815.
 Import NNnotations. 
 
diff --git a/theories/ordinals/Ackermann/NewNotations.v b/theories/ordinals/Ackermann/NewNotations.v
index c0673e18..b4a8e3cc 100644
--- a/theories/ordinals/Ackermann/NewNotations.v
+++ b/theories/ordinals/Ackermann/NewNotations.v
@@ -1,5 +1,5 @@
 From Coq Require Import Ensembles. 
-Require Import folProp. 
+From hydras.Ackermann Require Import folProp. 
 
 Notation "'SetAdds' E0  x1 .. xn" := 
   (Ensembles.Add _ (.. (Ensembles.Add _ E0 x1) .. ) xn) 
diff --git a/theories/ordinals/Ackermann/PA.v b/theories/ordinals/Ackermann/PA.v
index 351f7f0c..e743e234 100644
--- a/theories/ordinals/Ackermann/PA.v
+++ b/theories/ordinals/Ackermann/PA.v
@@ -5,9 +5,9 @@
 *)
 
 From Coq Require Import Arith Lia Ensembles Decidable.
-Require Import folProp subAll folLogic3.
-Require Export Languages LNT.
-Require Import NewNotations.
+From hydras.Ackermann Require Import folProp subAll folLogic3.
+From hydras.Ackermann Require Export Languages LNT.
+From hydras.Ackermann Require Import NewNotations.
 
 
 
diff --git a/theories/ordinals/Ackermann/PAconsistent.v b/theories/ordinals/Ackermann/PAconsistent.v
index a9844f93..cea20d87 100644
--- a/theories/ordinals/Ackermann/PAconsistent.v
+++ b/theories/ordinals/Ackermann/PAconsistent.v
@@ -3,7 +3,7 @@
     Original file by Russel O' Connor *)
 
 From Coq Require Import Arith.
-Require Import folProof  folProp  PA model.
+From hydras.Ackermann Require Import folProof  folProp  PA model.
 
 Definition natModel : Model LNT :=
   model LNT nat
diff --git a/theories/ordinals/Ackermann/PAtheory.v b/theories/ordinals/Ackermann/PAtheory.v
index 6c0922f3..0c107a7a 100644
--- a/theories/ordinals/Ackermann/PAtheory.v
+++ b/theories/ordinals/Ackermann/PAtheory.v
@@ -6,9 +6,9 @@
 
 From Coq Require Import Ensembles List Arith Lia.
 
-Require Import subAll folReplace folProp folLogic3 NN LNN2LNT.
-Require Export PA.
-Require Import NewNotations.
+From hydras.Ackermann Require Import subAll folReplace folProp folLogic3 NN LNN2LNT.
+From hydras.Ackermann Require Export PA.
+From hydras.Ackermann Require Import NewNotations.
 Import NNnotations.
 
 #[local] Arguments apply _ _ _ : clear implicits.
diff --git a/theories/ordinals/Ackermann/cPair.v b/theories/ordinals/Ackermann/cPair.v
index 65376b1a..79439e40 100644
--- a/theories/ordinals/Ackermann/cPair.v
+++ b/theories/ordinals/Ackermann/cPair.v
@@ -2,7 +2,7 @@
     (Originally  Russel O'Connors [goedel] contrib  *)
 
 
-Require Import Arith Coq.Lists.List Lia.
+From Coq Require Import Arith Lists.List Lia.
 From hydras Require Import extEqualNat primRec.
 From hydras Require Export Compat815 ssrnat_extracts.
 Import PRNotations.
diff --git a/theories/ordinals/Ackermann/checkPrf.v b/theories/ordinals/Ackermann/checkPrf.v
index bc754e0d..9a749af6 100644
--- a/theories/ordinals/Ackermann/checkPrf.v
+++ b/theories/ordinals/Ackermann/checkPrf.v
@@ -5,9 +5,10 @@
 *)
 
 From Coq Require Import Arith Lia. 
-Require Import primRec codeFreeVar codeSubFormula  cPair.
-Require Import code  folProp extEqualNat  wellFormed  folProof.
-Require Import prLogic  Compat815.
+From hydras.Ackermann Require Import primRec codeFreeVar 
+  codeSubFormula  cPair code  folProp extEqualNat  wellFormed 
+  folProof prLogic.
+From hydras Require Import  Compat815.
 From LibHyps Require Export LibHyps.
 From hydras Require Export MoreLibHyps NewNotations.
 Import LispAbbreviations. 
diff --git a/theories/ordinals/Ackermann/code.v b/theories/ordinals/Ackermann/code.v
index 3200d94e..63f5bb49 100644
--- a/theories/ordinals/Ackermann/code.v
+++ b/theories/ordinals/Ackermann/code.v
@@ -5,7 +5,7 @@ Original script by Russel O'Connor
  *)
 
 From Coq Require Import Arith.
-Require Import fol folProof cPair.
+From hydras.Ackermann Require Import fol folProof cPair.
 
 Section Code_Term_Formula_Proof.
 
diff --git a/theories/ordinals/Ackermann/codeFreeVar.v b/theories/ordinals/Ackermann/codeFreeVar.v
index 59ffd17b..0be967c4 100644
--- a/theories/ordinals/Ackermann/codeFreeVar.v
+++ b/theories/ordinals/Ackermann/codeFreeVar.v
@@ -4,11 +4,11 @@
 
 
 
-Require Import primRec  cPair.
+From hydras.Ackermann Require Import primRec  cPair.
 From Coq Require Import List Arith.
-Require Import ListExt.
-Require Export codeList.
-Require Import folProp  code Compat815.
+From hydras.Ackermann Require Import ListExt.
+From hydras.Ackermann Require Export codeList.
+From hydras Require Import folProp  code Compat815.
 Import LispAbbreviations.
 Import PRNotations.
 
diff --git a/theories/ordinals/Ackermann/codeList.v b/theories/ordinals/Ackermann/codeList.v
index 2bbdb250..4a431e2f 100644
--- a/theories/ordinals/Ackermann/codeList.v
+++ b/theories/ordinals/Ackermann/codeList.v
@@ -3,12 +3,12 @@
      Original script by Russel O'Connor 
 *)
 
-Require Import primRec  cPair.
-Require Export Coq.Lists.List.
-Require Import ListExt.
+From hydras.Ackermann Require Import primRec  cPair.
+From Coq Require Export Lists.List.
+From hydras.Ackermann Require Import ListExt.
 From Coq Require Import Arith.
-Require Vector.
-Require Import extEqualNat Compat815.
+From Coq Require Vector.
+From hydras Require Import extEqualNat Compat815.
 
 Definition codeLength : nat -> nat :=
   evalStrongRec 0
diff --git a/theories/ordinals/Ackermann/codeNatToTerm.v b/theories/ordinals/Ackermann/codeNatToTerm.v
index eceae3bc..9bd5aeaa 100644
--- a/theories/ordinals/Ackermann/codeNatToTerm.v
+++ b/theories/ordinals/Ackermann/codeNatToTerm.v
@@ -1,22 +1,17 @@
-Require Import primRec.
-Require Import cPair.
-Require Import Arith.
-Require Import code.
-Require Import folProp.
-Require Import folProof.
-Require Import Languages.
-Require LNN. 
-Require LNT.
+From hydras.Ackermann Require Import primRec cPair code folProp folProof
+                      Languages.
+From Coq Require Import Arith.
+From hydras.Ackermann Require LNN LNT.
 
 Definition natToTermLNN := LNN.natToTerm.
 
 Definition natToTermLNT := LNT.natToTerm.
 
 Fixpoint codeNatToTerm (n: nat) : nat :=
- match n with
-  0 => cPair 4 0
-| S p => cPair 3 (S (cPair (codeNatToTerm p) 0))
-end. 
+  match n with
+    0 => cPair 4 0
+  | S p => cPair 3 (S (cPair (codeNatToTerm p) 0))
+  end. 
 
 #[global] Instance LcodeLNN : Lcode LNN codeLNTFunction codeLNNRelation.
 Proof.
diff --git a/theories/ordinals/Ackermann/codePA.v b/theories/ordinals/Ackermann/codePA.v
index e211f1ea..71df5651 100644
--- a/theories/ordinals/Ackermann/codePA.v
+++ b/theories/ordinals/Ackermann/codePA.v
@@ -6,9 +6,11 @@
 
 From Coq Require Import Ensembles List Arith Lia.
 From Coq Require Vector.
+Import Bool.
 
-Require Import primRec  cPair folProp code  codeList  codeFreeVar  
-extEqualNat prLogic  Compat815 codeNatToTerm.
+From hydras
+  Require Import primRec  cPair folProp code  codeList  codeFreeVar  
+  extEqualNat prLogic  codeNatToTerm Compat815. 
 
 Import LispAbbreviations. 
 
@@ -133,8 +135,7 @@ Qed.
 
 End close.
 
-Require Import PA.
-Require Import codeSubFormula.
+From hydras.Ackermann Require Import PA codeSubFormula.
 
 Section Code_PA.
 
diff --git a/theories/ordinals/Ackermann/codeSubFormula.v b/theories/ordinals/Ackermann/codeSubFormula.v
index 9d2ad132..e4492b60 100644
--- a/theories/ordinals/Ackermann/codeSubFormula.v
+++ b/theories/ordinals/Ackermann/codeSubFormula.v
@@ -7,15 +7,17 @@
 From Coq Require Import Arith Vector Lia.
 From  Coq Require Vector.
 
-Require Import primRec  cPair folProp code extEqualNat.
 
-Require Import codeSubTerm codeFreeVar Compat815.
+From hydras.Ackermann 
+  Require Import primRec  cPair folProp code extEqualNat codeSubTerm 
+  codeFreeVar.
 
 Import LispAbbreviations.
 Import PRNotations. 
 
 From LibHyps Require Export LibHyps.
-From hydras Require Export MoreLibHyps NewNotations.
+From hydras Require Export MoreLibHyps NewNotations Compat815.
+Import Bool.
 
 Section Code_Substitute_Formula.
 
diff --git a/theories/ordinals/Ackermann/codeSubTerm.v b/theories/ordinals/Ackermann/codeSubTerm.v
index f87b4663..3af85170 100644
--- a/theories/ordinals/Ackermann/codeSubTerm.v
+++ b/theories/ordinals/Ackermann/codeSubTerm.v
@@ -1,11 +1,8 @@
-Require Import primRec.
-Require Import cPair.
-Require Import Arith.
-Require Import folProp.
-Require Import code.
-Require Import extEqualNat.
-Require Vector.
-Require Import Compat815.
+From hydras.Ackermann Require Import  primRec cPair folProp code 
+                        extEqualNat.
+From Coq Require Import Arith.
+From Coq  Require Vector.
+From hydras Require Import Compat815.
 Import LispAbbreviations. 
 Require Import NewNotations.
 Import PRNotations.
diff --git a/theories/ordinals/Ackermann/expressible.v b/theories/ordinals/Ackermann/expressible.v
index 5d3e07e1..3bcc0a3f 100644
--- a/theories/ordinals/Ackermann/expressible.v
+++ b/theories/ordinals/Ackermann/expressible.v
@@ -5,9 +5,9 @@
 
 
 From Coq Require Import Arith List.
-
-Require Import ListExt folProp subProp extEqualNat Languages LNN.
-Require Import NewNotations.
+From hydras.Ackermann 
+  Require Import ListExt folProp subProp extEqualNat Languages LNN
+  NewNotations.
 Import NNnotations.
 
 #[local] Arguments apply _ _ _ : clear implicits.
diff --git a/theories/ordinals/Ackermann/extEqualNat.v b/theories/ordinals/Ackermann/extEqualNat.v
index b2fc5e62..715c3b7a 100644
--- a/theories/ordinals/Ackermann/extEqualNat.v
+++ b/theories/ordinals/Ackermann/extEqualNat.v
@@ -5,7 +5,7 @@
      
 
 
-Require Import Arith.
+From Coq Require Import Arith.
 
 (* begin snippet naryFunc *)
 
diff --git a/theories/ordinals/Ackermann/fol.v b/theories/ordinals/Ackermann/fol.v
index 09086765..4eb8d211 100644
--- a/theories/ordinals/Ackermann/fol.v
+++ b/theories/ordinals/Ackermann/fol.v
@@ -10,7 +10,7 @@ This file is Public Domain
 From Coq Require Import Lists.List  Ensembles  Peano_dec  Eqdep_dec
   Arith Compare_dec Utf8.
 
-Require Import misc  Compat815 (* provisional *).
+From hydras Require Import Ackermann.misc  Compat815 (* provisional *).
 (* end hide *)
 
 (** *  First Order Formulas over a language *)
diff --git a/theories/ordinals/Ackermann/folLogic.v b/theories/ordinals/Ackermann/folLogic.v
index b4fb2162..c4e0f49b 100644
--- a/theories/ordinals/Ackermann/folLogic.v
+++ b/theories/ordinals/Ackermann/folLogic.v
@@ -5,7 +5,7 @@
 
 From Coq Require Import Ensembles List.
 
-Require Import ListExt folProof folProp Deduction.
+From hydras.Ackermann Require Import ListExt folProof folProp Deduction.
 Import FolNotations.
 
 Section Logic_Rules.
diff --git a/theories/ordinals/Ackermann/folLogic2.v b/theories/ordinals/Ackermann/folLogic2.v
index 0808450c..a679ef64 100644
--- a/theories/ordinals/Ackermann/folLogic2.v
+++ b/theories/ordinals/Ackermann/folLogic2.v
@@ -6,7 +6,8 @@
 
 From Coq Require Import Ensembles List  Arith.
 
-Require Import ListExt folProp folProof folLogic subProp folReplace.
+From hydras.Ackermann Require Import ListExt folProp folProof 
+  folLogic subProp folReplace.
 Import FolNotations.
 
 Section More_Logic_Rules.
diff --git a/theories/ordinals/Ackermann/folLogic3.v b/theories/ordinals/Ackermann/folLogic3.v
index ddb4ccc8..c8e83bd6 100644
--- a/theories/ordinals/Ackermann/folLogic3.v
+++ b/theories/ordinals/Ackermann/folLogic3.v
@@ -7,11 +7,11 @@
 From Coq Require Import Ensembles List Arith Lia.
 From LibHyps Require Export LibHyps.
 
-Require Import ListExt folProp folProof.
-Require Export folLogic folLogic2.
-Require Import subProp folReplace subAll misc.
-Require Import Compat815.
-Require Export MoreLibHyps. 
+From hydras.Ackermann Require Import ListExt folProp folProof.
+From hydras.Ackermann Require Export folLogic folLogic2.
+From hydras.Ackermann Require Import subProp folReplace subAll misc.
+From hydras Require Import Compat815.
+From hydras Require Export MoreLibHyps. 
 Import FolNotations.
 
 Section Equality_Logic_Rules.
diff --git a/theories/ordinals/Ackermann/folProof.v b/theories/ordinals/Ackermann/folProof.v
index bcf8c3ff..44862014 100644
--- a/theories/ordinals/Ackermann/folProof.v
+++ b/theories/ordinals/Ackermann/folProof.v
@@ -8,8 +8,8 @@
 From Coq Require Import Ensembles Lists.List Arith. 
 Import ListNotations. 
 
-Require Export fol.
-Require Import folProp.
+From hydras.Ackermann Require Export fol.
+From hydras.Ackermann Require Import folProp.
 Import FolNotations.
 
 
diff --git a/theories/ordinals/Ackermann/folProp.v b/theories/ordinals/Ackermann/folProp.v
index b8942770..dd69705f 100644
--- a/theories/ordinals/Ackermann/folProp.v
+++ b/theories/ordinals/Ackermann/folProp.v
@@ -1,8 +1,8 @@
 (******************************************************************************)
 From Coq Require Import Wf_nat Arith Lists.List Peano_dec. 
 
-Require Import ListExt. 
-Require Export fol.
+From hydras.Ackermann Require Import ListExt. 
+From hydras.Ackermann Require Export fol.
 Import FolNotations.
 
 Section Fol_Properties.
diff --git a/theories/ordinals/Ackermann/folReplace.v b/theories/ordinals/Ackermann/folReplace.v
index 4f38d15a..6ccc99ae 100644
--- a/theories/ordinals/Ackermann/folReplace.v
+++ b/theories/ordinals/Ackermann/folReplace.v
@@ -1,11 +1,7 @@
-Require Import Ensembles.
-Require Import Coq.Lists.List.
-Require Import Peano_dec.
-
-Require Import ListExt.
-Require Import folProof.
-Require Import folLogic.
-Require Import folProp.
+From Coq Require Import Ensembles Lists.List Peano_dec.
+
+From hydras.Ackermann 
+  Require Import ListExt folProof folLogic folProp.
 
 Section Replacement.
 
diff --git a/theories/ordinals/Ackermann/misc.v b/theories/ordinals/Ackermann/misc.v
index e39bc35b..23d2b689 100644
--- a/theories/ordinals/Ackermann/misc.v
+++ b/theories/ordinals/Ackermann/misc.v
@@ -1,4 +1,4 @@
-Require Export Eqdep_dec.
+From Coq Require Export Eqdep_dec.
 
 #[global] Set Asymmetric Patterns. 
 
diff --git a/theories/ordinals/Ackermann/model.v b/theories/ordinals/Ackermann/model.v
index 05d5da19..5291ac39 100644
--- a/theories/ordinals/Ackermann/model.v
+++ b/theories/ordinals/Ackermann/model.v
@@ -6,13 +6,11 @@
 
 From Coq Require Import Ensembles List Vector Arith.
 
-Require Import ListExt.
-Require Import folProof.
-Require Import folProp.
-Require Import Peano_dec.
-Require Import misc.
+From hydras.Ackermann Require Import ListExt folProof folProp.
+From Coq Require Import Peano_dec.
+From hydras.Ackermann Require Import misc.
 Import FolNotations.
-Require Import NewNotations.
+From hydras.Ackermann Require Import NewNotations.
 
 Section Model_Theory.
 
diff --git a/theories/ordinals/Ackermann/prLogic.v b/theories/ordinals/Ackermann/prLogic.v
index 3f28b980..e0f13642 100644
--- a/theories/ordinals/Ackermann/prLogic.v
+++ b/theories/ordinals/Ackermann/prLogic.v
@@ -6,7 +6,7 @@
      are JUST  helpers to prove that the encoding of basic FOL connectives are PR *)
 
 
-Require Import primRec code cPair.
+From hydras.Ackermann Require Import primRec code cPair.
 From Coq Require Import Arith.
 
 Lemma codeForallIsPR : isPR 2 (fun a b : nat => cPair 3 (cPair a b)).
diff --git a/theories/ordinals/Ackermann/primRec.v b/theories/ordinals/Ackermann/primRec.v
index 6d7c3e00..b8d1b526 100644
--- a/theories/ordinals/Ackermann/primRec.v
+++ b/theories/ordinals/Ackermann/primRec.v
@@ -1,18 +1,10 @@
 (** Primitive Recursive functions *)
 (** Russel O'Connor *)
 
-Require Import Arith.
-Require Import Peano_dec.
-Require Import Compare_dec.
-Require Import Coq.Lists.List.
-Require Import Eqdep_dec.
-Require Import Utf8.
+From Coq Require Import Arith Peano_dec Compare_dec List Eqdep_dec Utf8.
 From hydras Require Import extEqualNat misc Compat815.
-Require Vector.
-
-Require Export Bool.
-Require Export EqNat.
-Require Import Lia. 
+From Coq Require Vector Bool EqNat.
+From  Coq Require Import Lia. 
 
 
 (** * Definitions *)
@@ -1019,7 +1011,7 @@ Qed.
 Definition orRel (n : nat) (R S : naryRel n) : naryRel n.
 Proof. 
   induction n as [| n Hrecn].
-  - apply (R || S).
+  - apply (R || S)%bool.
   - cbn in |- *;intros H; apply Hrecn.
     + apply (R H).
     + apply (S H).
@@ -1061,7 +1053,7 @@ Qed.
 Definition andRel (n : nat) (R S : naryRel n) : naryRel n.
 Proof. 
   induction n as [| n Hrecn].
-  - exact (R && S).
+  - exact (R && S)%bool.
   - simpl in |- *; intros; apply Hrecn.
     + apply (R H).
     + apply (S H).
diff --git a/theories/ordinals/Ackermann/subAll.v b/theories/ordinals/Ackermann/subAll.v
index 82f43b33..d8da6d70 100644
--- a/theories/ordinals/Ackermann/subAll.v
+++ b/theories/ordinals/Ackermann/subAll.v
@@ -5,8 +5,9 @@
 
 From Coq Require Import Ensembles List Arith  Peano_dec.
 
-Require Import ListExt folProof folLogic folLogic2 folProp.
-Require Import folReplace  subProp Compat815.
+From hydras.Ackermann Require Import ListExt folProof folLogic 
+  folLogic2 folProp.
+From hydras Require Import folReplace  subProp Compat815.
 From Coq Require Import Lia.
 Import FolNotations.
 
diff --git a/theories/ordinals/Ackermann/subProp.v b/theories/ordinals/Ackermann/subProp.v
index 94cd45dc..928d9722 100644
--- a/theories/ordinals/Ackermann/subProp.v
+++ b/theories/ordinals/Ackermann/subProp.v
@@ -1,13 +1,9 @@
-Require Import Ensembles.
-Require Import Coq.Lists.List.
-Require Import Peano_dec.
-Require Import ListExt.
-Require Import Arith.
+From Coq Require Import Ensembles List Peano_dec.
+From hydras.Ackermann Require Import ListExt.
+From Coq Require Import Arith.
 
-Require Import folProof.
-Require Import folLogic.
-Require Import folProp.
-Require Import folReplace.
+From hydras.Ackermann 
+  Require Import folProof folLogic folProp folReplace.
 
 From LibHyps Require Export LibHyps.
 From hydras Require Export MoreLibHyps NewNotations.
diff --git a/theories/ordinals/Ackermann/wConsistent.v b/theories/ordinals/Ackermann/wConsistent.v
index 9d1df5f2..22dec24e 100644
--- a/theories/ordinals/Ackermann/wConsistent.v
+++ b/theories/ordinals/Ackermann/wConsistent.v
@@ -1,8 +1,6 @@
-Require Import folProof.
-Require Import Arith.
-Require Import folProp.
-Require Import LNN.
-Require Import Coq.Lists.List.
+From hydras.Ackermann Require Import folProof folProp LNN.
+From Coq Require Import Arith List.
+
 Import NNnotations. 
 
 Definition wConsistent (T : System) :=
diff --git a/theories/ordinals/Ackermann/wellFormed.v b/theories/ordinals/Ackermann/wellFormed.v
index bb89e3bb..360ef743 100644
--- a/theories/ordinals/Ackermann/wellFormed.v
+++ b/theories/ordinals/Ackermann/wellFormed.v
@@ -1,13 +1,11 @@
 
-Require Import primRec.
-Require Import cPair.
-Require Import Arith Lia.
-Require Import code.
-Require Import folProp.
-Require Import extEqualNat.
-Require Import codeList.
-Require Import Compat815.
+From hydras.Ackermann Require Import primRec cPair.
+From Coq Require Import Arith Lia.
+From hydras.Ackermann Require Import code folProp 
+  extEqualNat codeList.
+From hydras Require Import Compat815.
 Import LispAbbreviations. 
+
 Section Well_Formed_Term.
 
 Variable L : Language.
diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v
index afc4bca7..67f933d0 100644
--- a/theories/ordinals/Epsilon0/Canon.v
+++ b/theories/ordinals/Epsilon0/Canon.v
@@ -980,7 +980,7 @@ Lemma canonS_LE alpha n :
   
   (** exercise  after Guillaume Melquiond   *)
   
-  Require Import Fuel. 
+ From hydras  Require Import Fuel. 
 
 Fixpoint  approx alpha beta fuel i :=
   match fuel with
diff --git a/theories/ordinals/Epsilon0/Hprime.v b/theories/ordinals/Epsilon0/Hprime.v
index 9618747b..6838c962 100644
--- a/theories/ordinals/Epsilon0/Hprime.v
+++ b/theories/ordinals/Epsilon0/Hprime.v
@@ -20,7 +20,7 @@ From Coq Require Import ArithRing Lia.
 From hydras Require Import  E0    Canon Paths.
 From hydras Require Import Exp2 Iterates Simple_LexProd.
 Import RelationClasses Relations.
-Require Import Compat815. 
+From hydras Require Import Compat815. 
 From Equations Require Import Equations.
 
  Open Scope E0_scope.
diff --git a/theories/ordinals/Epsilon0/L_alpha.v b/theories/ordinals/Epsilon0/L_alpha.v
index 78f120fd..306894f2 100644
--- a/theories/ordinals/Epsilon0/L_alpha.v
+++ b/theories/ordinals/Epsilon0/L_alpha.v
@@ -255,6 +255,6 @@ Proof with auto with E0.
        rewrite H'_eq2, L_succ_eqn ...
 Qed.
 
-Require Import Extraction.
+From Coq Require Import Extraction.
 
 Recursive Extraction L_.
diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v
index b36c4331..9f99fc17 100644
--- a/theories/ordinals/Epsilon0/T1.v
+++ b/theories/ordinals/Epsilon0/T1.v
@@ -108,7 +108,7 @@ Fixpoint T1limit alpha :=
   match alpha with
     | zero => false
     | cons zero _ _ => false
-    | cons alpha _ zero => true
+    | cons _ _ zero => true
     | cons _ _ beta => T1limit beta
   end.
 
@@ -636,7 +636,7 @@ Fixpoint minus (alpha beta : T1) :T1 :=
      then zero
      else  cons zero (Peano.pred (n-n')) zero
  |  cons zero n _, zero =>  cons zero n zero
- |  cons zero n _, y =>  zero
+ |  cons zero _ _, y =>  zero
  |  cons a n b, zero =>  cons a n b
  |  cons a n b, cons a' n' b' =>
      (match compare a a' with
diff --git a/theories/ordinals/Hydra/Hydra_Theorems.v b/theories/ordinals/Hydra/Hydra_Theorems.v
index 1ff1b631..d521ef4a 100644
--- a/theories/ordinals/Hydra/Hydra_Theorems.v
+++ b/theories/ordinals/Hydra/Hydra_Theorems.v
@@ -108,8 +108,8 @@ Print Assumptions battle_length_std.
 
 (** ** Battle length is not PR *)
 
-Require Import primRec F_alpha  AckNotPR PrimRecExamples.
-Require Import F_omega.
+From hydras Require Import primRec F_alpha  AckNotPR 
+  PrimRecExamples F_omega.
 Import E0.
 
 (* begin snippet battleLengthNotPRa *)
diff --git a/theories/ordinals/Hydra/KP_example.v b/theories/ordinals/Hydra/KP_example.v
index 0219adff..c3f2da5c 100644
--- a/theories/ordinals/Hydra/KP_example.v
+++ b/theories/ordinals/Hydra/KP_example.v
@@ -1,6 +1,6 @@
 (** Pierre Casteran, Univ. Bordeaux and LaBRI  *)
 
- Require Import Hydra_Definitions Hydra_Lemmas.
+ From hydras Require Import Hydra_Definitions Hydra_Lemmas.
 
 (** The hydra from page 286 of [KP] *)
 
diff --git a/theories/ordinals/MoreAck/Ack.v b/theories/ordinals/MoreAck/Ack.v
index 0db74790..a111bd31 100644
--- a/theories/ordinals/MoreAck/Ack.v
+++ b/theories/ordinals/MoreAck/Ack.v
@@ -1,7 +1,6 @@
 From hydras Require Export Iterates Exp2.
 From Coq Require Import Lia.
-Require Import Coq.Program.Wf.
-Require Import Coq.Arith.Arith.
+From Coq Require Import Program.Wf Arith.
 From hydras Require Import ssrnat_extracts.
 
 
diff --git a/theories/ordinals/MoreAck/AckNotPR.v b/theories/ordinals/MoreAck/AckNotPR.v
index f1dba83a..67d458d4 100644
--- a/theories/ordinals/MoreAck/AckNotPR.v
+++ b/theories/ordinals/MoreAck/AckNotPR.v
@@ -7,10 +7,9 @@ and
  *)
 
 Set Apply With Renaming.
-
-Require Import primRec Arith ArithRing List Ack MoreVectors Lia.
-Require Import Compare_dec.
-Import extEqualNat  VectorNotations.
+From hydras Require Import primRec Ack MoreVectors.
+From Coq Require Import  Arith ArithRing List Lia Compare_dec.
+Import extEqualNat  VectorNotations Vector.
 
 
 
@@ -27,15 +26,15 @@ Import extEqualNat  VectorNotations.
 
 Notation "'v_apply' f v" := (evalList _ v f) (at level 10, f at level 9).
 
-
+Check [4].
 Example Ex2 : forall (f: naryFunc 2) x y,
-    v_apply f (x::y::nil) = f x y.
+    v_apply f [x;y] = f x y.
 Proof.
   intros; now cbn.
 Qed.
 
 Example Ex4 : forall (f: naryFunc 4) x y z t,
-    v_apply f (x::y::z::t::nil) = f x y z t.
+    v_apply f [x;y;z;t] = f x y z t.
 Proof.
   intros; now cbn.
 Qed.
@@ -59,7 +58,7 @@ Definition majorizedPR {n} (x: PrimRec n) A :=
 Definition majorizedS {n m} (fs : Vector.t (naryFunc n) m)
            (A : naryFunc 2):=
   exists N, forall (v: t nat n),
-      max_v (map (fun f => v_apply f v) fs) <= A N (max_v v).
+      max_v (Vector.map (fun f => v_apply f v) fs) <= A N (max_v v).
 
 Definition majorizedSPR {n m} (x : PrimRecs n m) :=
   majorizedS (evalPrimRecs _ _ x).
@@ -73,7 +72,7 @@ Section evalList.
     v_apply (evalConstFunc n x) v = x.
     Proof.
     induction n; cbn.
-    - intros; cbn ; replace v with (@nil nat).
+    - intros; cbn ; replace v with (@Vector.nil nat).
       + now  cbn.
       +  symmetry; apply t_0_nil.
     - intros; cbn; rewrite (decomp _ _ v); cbn; auto.
diff --git a/theories/ordinals/MoreAck/BadSubst.v b/theories/ordinals/MoreAck/BadSubst.v
index b5cb1676..8be573e0 100644
--- a/theories/ordinals/MoreAck/BadSubst.v
+++ b/theories/ordinals/MoreAck/BadSubst.v
@@ -1,5 +1,5 @@
-Require Import fol folProp folProof  Languages folLogic Arith.
-Require Import primRec.
+From hydras Require Import fol folProp folProof  Languages folLogic primRec.
+From Coq Require Import Arith.
 
 Import FolNotations. 
 
@@ -25,7 +25,7 @@ Module BadSubst.
 End BadSubst. 
 (* end snippet BadSubstFdef *)
 
-Require Import List.
+From Coq Require Import List.
 Import ListNotations.
 
 Module BadSubstF2. 
@@ -46,7 +46,7 @@ Fail Fixpoint substF L (F : Formula L) v (t: Term L) :=
 
 End BadSubstF2.
 
-Require Import FolExamples. 
+From hydras Require Import FolExamples. 
 Import Toy. 
 
 (* begin snippet BadSubstFexample *)
diff --git a/theories/ordinals/MoreAck/FolExamples.v b/theories/ordinals/MoreAck/FolExamples.v
index 46912065..46150291 100644
--- a/theories/ordinals/MoreAck/FolExamples.v
+++ b/theories/ordinals/MoreAck/FolExamples.v
@@ -2,9 +2,9 @@
 
 From Coq Require Import Arith Lists.List.
 
-Require Import fol folProp folProof  Languages folLogic 
-  folLogic2 folLogic3 subAll Deduction.
-Require Import primRec.
+From hydras.Ackermann 
+  Require Import fol folProp folProof  Languages folLogic 
+  folLogic2 folLogic3 subAll Deduction primRec.
 Import ListNotations. 
 Import FolNotations. 
 
diff --git a/theories/ordinals/MoreAck/Iterate_compat.v b/theories/ordinals/MoreAck/Iterate_compat.v
index 4006eaf8..875d0ff4 100644
--- a/theories/ordinals/MoreAck/Iterate_compat.v
+++ b/theories/ordinals/MoreAck/Iterate_compat.v
@@ -1,7 +1,7 @@
 (** Compatibility between primRec.iterate and Iterates.iterate *)
 
-Require primRec Iterates.
-Require Import extEqualNat.
+From hydras Require primRec Iterates.
+From hydras.Ackermann Require Import extEqualNat.
 
 (*
 
diff --git a/theories/ordinals/MoreAck/expressibleExamples.v b/theories/ordinals/MoreAck/expressibleExamples.v
index 0ee58ee9..6c94e85f 100644
--- a/theories/ordinals/MoreAck/expressibleExamples.v
+++ b/theories/ordinals/MoreAck/expressibleExamples.v
@@ -1,7 +1,6 @@
 From hydras.Ackermann Require Import expressible.
 
-Require Import NN. 
-Require Import NewNotations NNtheory. 
+From hydras.Ackermann Require Import NN NewNotations NNtheory. 
 Import NNnotations.
 From Coq Require Import Lia. 
 
diff --git a/theories/ordinals/OrdinalNotations/ON_Finite.v b/theories/ordinals/OrdinalNotations/ON_Finite.v
index 4a2392a0..c969d12d 100644
--- a/theories/ordinals/OrdinalNotations/ON_Finite.v
+++ b/theories/ordinals/OrdinalNotations/ON_Finite.v
@@ -8,7 +8,7 @@ From Coq Require Import Arith Relations Lia Logic.Eqdep_dec Ensembles
         RelationClasses.
 From hydras Require Import ON_Generic.
 
-Require Wf_nat.
+From Coq Require Wf_nat.
 
 
 
diff --git a/theories/ordinals/OrdinalNotations/ON_Generic.v b/theories/ordinals/OrdinalNotations/ON_Generic.v
index af84dbf6..4deb639b 100644
--- a/theories/ordinals/OrdinalNotations/ON_Generic.v
+++ b/theories/ordinals/OrdinalNotations/ON_Generic.v
@@ -9,7 +9,7 @@ From hydras Require Import  OrdNotations Schutte_basics.
 From Coq Require Export Wellfounded.Inverse_Image Wellfounded.Inclusion.
 Import Relation_Definitions.
 From hydras Require Export MoreOrders.
-Require Export Comparable.
+From hydras Require Export Comparable.
   
 Generalizable All Variables.
 Declare Scope ON_scope.
diff --git a/theories/ordinals/OrdinalNotations/OmegaOmega.v b/theories/ordinals/OrdinalNotations/OmegaOmega.v
index a36c5c50..799f8f8b 100644
--- a/theories/ordinals/OrdinalNotations/OmegaOmega.v
+++ b/theories/ordinals/OrdinalNotations/OmegaOmega.v
@@ -2,14 +2,11 @@
 
 (** New implementation as a refinement of epsilon0 *)
 
-Require Import T1 E0.
-Require Import Arith  Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec
+From hydras Require Import T1 E0 Comparable.
+From Coq Require Import Arith  Logic.Eqdep_dec Peano_dec
   List Bool
-  Recdef Lia  Coq.Wellfounded.Inverse_Image
-  Coq.Wellfounded.Inclusion RelationClasses  Logic.Eqdep_dec.
-
-
-Require Import Comparable.
+  Recdef Lia Wellfounded.Inverse_Image
+  Wellfounded.Inclusion RelationClasses .
 
 (** * Representation by lists of pairs of integers *)
 
diff --git a/theories/ordinals/Prelude/Comparable.v b/theories/ordinals/Prelude/Comparable.v
index aac0bd1a..86085c7b 100644
--- a/theories/ordinals/Prelude/Comparable.v
+++ b/theories/ordinals/Prelude/Comparable.v
@@ -1,5 +1,5 @@
 From Coq Require Import Relations RelationClasses Setoid.
-Require Export MoreOrders STDPP_compat.
+From hydras Require Export MoreOrders STDPP_compat.
 
 (* begin snippet ComparableDef:: no-out *)
 Class Compare (A:Type) := compare : A -> A -> comparison.
diff --git a/theories/ordinals/Prelude/Compat815.v b/theories/ordinals/Prelude/Compat815.v
index 87e84d5b..2f824007 100644
--- a/theories/ordinals/Prelude/Compat815.v
+++ b/theories/ordinals/Prelude/Compat815.v
@@ -1,6 +1,6 @@
 (** provisionally fixes some compatibilty issues 8.15 -> 8.16 *)
 
-Require Import Arith Lia.
+From Coq Require Import Arith Lia.
 Import Nat.
 
 
diff --git a/theories/ordinals/Prelude/DecPreOrder.v b/theories/ordinals/Prelude/DecPreOrder.v
index f802819c..b9c9817f 100644
--- a/theories/ordinals/Prelude/DecPreOrder.v
+++ b/theories/ordinals/Prelude/DecPreOrder.v
@@ -9,7 +9,7 @@ From Coq Require Export Relations RelationClasses Setoid.
 Class Total {A:Type}(R: relation A) :=
   totalness : forall a b:A, R a b \/ R b a.
 
-Require Export STDPP_compat.
+From hydras Require Export STDPP_compat.
 
 
 #[ global ] Instance comparison_eq_dec : EqDecision comparison.
diff --git a/theories/ordinals/Prelude/Fuel.v b/theories/ordinals/Prelude/Fuel.v
index 3a069cf5..89cff1a9 100644
--- a/theories/ordinals/Prelude/Fuel.v
+++ b/theories/ordinals/Prelude/Fuel.v
@@ -1,7 +1,7 @@
 
 (* Robert Krebbers's trick  *)
 
-Require Import FunInd Recdef Wf_nat Lia.
+From Coq Require Import FunInd Recdef Wf_nat Lia.
 
 Function zero (n:nat)  {wf lt n} : nat :=
   match n with
diff --git a/theories/ordinals/Prelude/LibHyps_Experiments.v b/theories/ordinals/Prelude/LibHyps_Experiments.v
index 0edf3703..c013d73b 100644
--- a/theories/ordinals/Prelude/LibHyps_Experiments.v
+++ b/theories/ordinals/Prelude/LibHyps_Experiments.v
@@ -1,9 +1,9 @@
 From LibHyps Require Export LibHyps.
-Require Export MoreLibHyps. 
+From hydras Require Export MoreLibHyps. 
 
 (*  move to experimental file (not to export *)
 
-Require Import List.
+From Coq Require Import List.
 Import ListNotations. 
 #[local] Open Scope autonaming_scope.
 
@@ -21,7 +21,7 @@ Goal forall n p , n <= p -> forall q, p <= q -> n <= q.
   - intros /n.  apply h_all_le_n_; transitivity (S m); auto.
 Qed.
 
-Require Import Arith. 
+From Coq Require Import Arith. 
 Parameters f g h : nat -> nat.
 Parameter P : nat->nat->nat-> Prop.
 Goal forall x y ,  f (g (h x)) = h (g (f y)) -> x = y -> x < y ->
diff --git a/theories/ordinals/Prelude/MoreLibHyps.v b/theories/ordinals/Prelude/MoreLibHyps.v
index 168f27e4..6c6c2d6d 100644
--- a/theories/ordinals/Prelude/MoreLibHyps.v
+++ b/theories/ordinals/Prelude/MoreLibHyps.v
@@ -7,7 +7,7 @@ Tactic Notation (at level 4) tactic4(Tac) "/" "r?" :=
   Tac ; {< fun h  => try revert h }.
 
 
-Require Import List.
+From Coq Require Import List.
 Import ListNotations. 
 #[local] Open Scope autonaming_scope.
 
diff --git a/theories/ordinals/Prelude/MoreLists.v b/theories/ordinals/Prelude/MoreLists.v
index 631b2621..86eac674 100644
--- a/theories/ordinals/Prelude/MoreLists.v
+++ b/theories/ordinals/Prelude/MoreLists.v
@@ -4,7 +4,7 @@
 
 
 From Coq  Require Export List Arith Relations Lia.
-Require Import Sorting.Sorted  Compare_dec  Sorting.Sorted.
+From Coq Require Import Sorting.Sorted  Compare_dec  Sorting.Sorted.
 
 (** *  Sets of natural numbers as lists *)
 
diff --git a/theories/ordinals/Prelude/MoreVectors.v b/theories/ordinals/Prelude/MoreVectors.v
index 765a5030..83993fdf 100644
--- a/theories/ordinals/Prelude/MoreVectors.v
+++ b/theories/ordinals/Prelude/MoreVectors.v
@@ -1,4 +1,4 @@
-Require Export Bool Arith Vector Lia.
+From Coq Require Export Bool Arith Vector Lia.
 Import Vector VectorNotations.
 
 (** generalities on vectors *)
diff --git a/theories/ordinals/Prelude/STDPP_compat.v b/theories/ordinals/Prelude/STDPP_compat.v
index a084ad1a..6c3d5465 100644
--- a/theories/ordinals/Prelude/STDPP_compat.v
+++ b/theories/ordinals/Prelude/STDPP_compat.v
@@ -1,4 +1,4 @@
-Require Import Relations.
+From Coq Require Import Relations.
 
 Class Assoc {A} (R : relation A) (f : A -> A -> A) : Prop :=
   assoc x y z : R (f x (f y z)) (f (f x y) z).
diff --git a/theories/ordinals/Schutte/Addition.v b/theories/ordinals/Schutte/Addition.v
index 09d74947..a7a1dd4e 100644
--- a/theories/ordinals/Schutte/Addition.v
+++ b/theories/ordinals/Schutte/Addition.v
@@ -4,7 +4,7 @@ From ZornsLemma Require Import CountableTypes.
 From hydras Require Export Schutte_basics  Ordering_Functions
      PartialFun  Countable  MoreEpsilonIota.
 Set Implicit Arguments.
-Require Export STDPP_compat.
+From hydras Require Export STDPP_compat.
 
 (** * Definitions *)
 
diff --git a/theories/ordinals/Schutte/CNF.v b/theories/ordinals/Schutte/CNF.v
index 01787c23..c8ec79a9 100644
--- a/theories/ordinals/Schutte/CNF.v
+++ b/theories/ordinals/Schutte/CNF.v
@@ -8,7 +8,7 @@ From Coq Require Import Arith List Sorting.Sorted
      Logic.Epsilon Ensembles.
 From hydras Require Export Schutte_basics  Ordering_Functions
      PartialFun  Countable Schutte.Addition AP.
-Require Export  Classical.
+From Coq Require Export  Classical.
 
 
 Set Implicit Arguments.
diff --git a/theories/ordinals/solutions_exercises/F_3.v b/theories/ordinals/solutions_exercises/F_3.v
index 41cca55c..a5bd5d2e 100644
--- a/theories/ordinals/solutions_exercises/F_3.v
+++ b/theories/ordinals/solutions_exercises/F_3.v
@@ -1,8 +1,8 @@
-Require Import Arith.
-Require Import Iterates F_alpha E0.
-Require Import ArithRing Lia   Max.
+From Coq Require Import Arith.
+From hydras Require Import Iterates F_alpha E0.
+From Coq Require Import ArithRing Lia   Max.
 Import Exp2.
-Require Import Compat815.
+From hydras Require Import Compat815.
 Open Scope nat_scope.
 
 Lemma LF3 : dominates_from 2 (F_ 3) (fun  n => iterate exp2 n n).
diff --git a/theories/ordinals/solutions_exercises/FibonacciPR.v b/theories/ordinals/solutions_exercises/FibonacciPR.v
index ae2e2a03..3e76e829 100644
--- a/theories/ordinals/solutions_exercises/FibonacciPR.v
+++ b/theories/ordinals/solutions_exercises/FibonacciPR.v
@@ -1,4 +1,4 @@
-Require Import primRec cPair extEqualNat.
+From hydras Require Import primRec cPair extEqualNat.
 
 (** The famous Fibonacci function *)
 
diff --git a/theories/ordinals/solutions_exercises/MultisetWf.v b/theories/ordinals/solutions_exercises/MultisetWf.v
index 0e824299..c0c4e622 100644
--- a/theories/ordinals/solutions_exercises/MultisetWf.v
+++ b/theories/ordinals/solutions_exercises/MultisetWf.v
@@ -1,7 +1,7 @@
 Set Implicit Arguments.
 Require Import Relations List Sorted Arith.
 From hydras Require Import Restriction.
-Require Import Lia.
+From Coq Require Import Lia.
 
 
 (* begin snippet tDef *)
diff --git a/theories/ordinals/solutions_exercises/OnCodeList.v b/theories/ordinals/solutions_exercises/OnCodeList.v
index cdaa2453..e3367d76 100644
--- a/theories/ordinals/solutions_exercises/OnCodeList.v
+++ b/theories/ordinals/solutions_exercises/OnCodeList.v
@@ -1,5 +1,6 @@
 (* begin snippet membersDef:: no-out *)
-Require Import primRec cPair Arith.
+From hydras.Ackermann Require Import primRec cPair.
+From Coq Require Import Arith.
 From Equations Require Import  Equations.
 
 Equations members (a:nat): list nat by wf a:=
diff --git a/theories/ordinals/solutions_exercises/is_F_monotonous.v b/theories/ordinals/solutions_exercises/is_F_monotonous.v
index 1de71fea..c4e55adb 100644
--- a/theories/ordinals/solutions_exercises/is_F_monotonous.v
+++ b/theories/ordinals/solutions_exercises/is_F_monotonous.v
@@ -1,7 +1,7 @@
-Require Import Iterates F_alpha E0.
-Require Import ArithRing Lia   Max.
+From hydras Require Import Iterates F_alpha E0.
+From Coq Require Import ArithRing Lia   Max.
 Import Exp2 Canon.
-Require Import Mult.
+From Coq Require Import Mult.
 Open Scope nat_scope.
 
 
diff --git a/theories/ordinals/solutions_exercises/omega_iterates.v b/theories/ordinals/solutions_exercises/omega_iterates.v
index 180e9068..260c7c1f 100644
--- a/theories/ordinals/solutions_exercises/omega_iterates.v
+++ b/theories/ordinals/solutions_exercises/omega_iterates.v
@@ -3,7 +3,7 @@
 (** Old stuff 
 *)
 
-Require Import ArithRing Lia Arith.
+From Coq Require Import ArithRing Lia Arith.
 Import Nat.
 
 Definition id_nat (n:nat) := n.