Adapt to coq/coq#19530

Kami/Decomposition.v

@@ -1,5 +1,5 @@
-Require Import Bool List String.
-Require Import Structures.Equalities FunctionalExtensionality Program.Equality Eqdep Eqdep_dec.
+From Coq Require Import Bool List String.
+From Coq Require Import Equalities FunctionalExtensionality Equality Eqdep Eqdep_dec.
 Require Import Lib.Struct Lib.Word Lib.CommonTactics Lib.ilist Lib.FMap.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.Wf Kami.RefinementFacts.
 

Kami/Duplicate.v

@@ -1,4 +1,4 @@
-Require Import Bool String List Arith.Peano_dec Lia.
+From Coq Require Import Bool String List Peano_dec Lia.
 Require Import Lib.FMap Lib.Struct Lib.CommonTactics Lib.Indexer Lib.StringEq Lib.ListSupport.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.RefinementFacts Kami.Renaming Kami.Wf.
 Require Import Kami.Specialize.

Kami/Ex/Divider32.v

@@ -3,7 +3,7 @@ Require Import Lib.CommonTactics Lib.NatLib Lib.Indexer
         Lib.Struct Lib.DepEq Lib.Word Lib.FMap Lib.Reflection.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics Kami.SemFacts Kami.Tactics.
 
-Require Import ZArith Eqdep Program.Equality.
+From Coq Require Import ZArith Eqdep Equality.
 
 Set Implicit Arguments.
 

Kami/Ex/Divider64.v

@@ -3,7 +3,7 @@ Require Import Lib.CommonTactics Lib.NatLib Lib.Indexer
         Lib.Struct Lib.DepEq Lib.Word Lib.FMap Lib.Reflection.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics Kami.SemFacts Kami.Tactics.
 
-Require Import ZArith Eqdep Program.Equality.
+Require Import ZArith Eqdep Equality.
 
 Set Implicit Arguments.
 

Kami/Ex/FifoCorrect.v

@@ -1,4 +1,4 @@
-Require Import Arith.Peano_dec Bool String List PeanoNat.
+Require Import Peano_dec Bool String List PeanoNat.
 Require Import Lib.CommonTactics Lib.ilist Lib.NatLib Lib.Word Lib.Struct Lib.StringEq.
 Require Import Lib.FMap Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.Wf Kami.RefinementFacts.

Kami/Ex/IsaRv32.v

@@ -1,4 +1,4 @@
-Require Import Bool String List Vector ZArith.BinInt.
+From Coq Require Import Bool String List Vector BinInt.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax Kami.Semantics Kami.Notations.
 Require Import Ex.MemTypes Ex.SC.

Kami/Ex/Multiplier32.v

@@ -3,7 +3,7 @@ Require Import Lib.CommonTactics Lib.NatLib Lib.Indexer
         Lib.Struct Lib.DepEq Lib.Word Lib.FMap Lib.Reflection.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics Kami.SemFacts Kami.Tactics.
 
-Require Import ZArith Eqdep Program.Equality.
+From Coq Require Import ZArith Eqdep Equality.
 
 Set Implicit Arguments.
 Open Scope string.

Kami/Ex/Multiplier64.v

@@ -3,7 +3,7 @@ Require Import Lib.CommonTactics Lib.NatLib Lib.Indexer
         Lib.Struct Lib.DepEq Lib.Word Lib.FMap Lib.Reflection.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics Kami.SemFacts Kami.Tactics.
 
-Require Import ZArith Eqdep Program.Equality.
+Require Import ZArith Eqdep Equality.
 
 Set Implicit Arguments.
 Open Scope string.

Kami/Ex/NativeFifo.v

@@ -1,4 +1,4 @@
-Require Import Arith.Peano_dec Bool String List.
+Require Import Peano_dec Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word Lib.Indexer Lib.StringAsList Lib.StringEq.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics.
 Require Import Kami.Wf Kami.Tactics.

Kami/Ex/SimpleFifoCorrect.v

@@ -1,4 +1,4 @@
-Require Import Arith.Peano_dec Bool String List PeanoNat.
+Require Import Peano_dec Bool String List PeanoNat.
 Require Import Lib.CommonTactics Lib.ilist Lib.NatLib Lib.Word Lib.Struct.
 Require Import Lib.FMap Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.RefinementFacts.

Kami/Lib/CommonTactics.v

@@ -1,5 +1,5 @@
-Require Import Bool Ascii String List Eqdep Lia.
-Require Import Logic.FunctionalExtensionality.
+From Coq Require Import Bool Ascii String List Eqdep Lia.
+From Coq Require Import FunctionalExtensionality.
 
 Ltac isNew P :=
   match goal with

Kami/Lib/DepEq.v

@@ -1,5 +1,6 @@
-Require Import Coq.Arith.PeanoNat.
-Require Import Coq.Logic.Eqdep Coq.Logic.Eqdep_dec Coq.Program.Equality.
+From Coq Require Import PeanoNat.
+From Coq Require Import Eqdep Eqdep_dec.
+From Coq.Program Require Import Equality.
 
 (** * Equalities on dependent types *)
 

Kami/Lib/FMap.v

@@ -1,9 +1,9 @@
-Require Import String.
-Require FSets.FMapList FSets.FMapFacts.
-Require Import Lists.SetoidList.
-Require Import Structures.OrderedType.
-Require Import Structures.OrderedTypeEx.
-Require Import Equalities Eqdep_dec FMapInterface.
+From Coq Require Import String.
+From Coq Require FMapList FMapFacts.
+From Coq Require Import SetoidList.
+From Coq Require Import OrderedType.
+From Coq Require Import OrderedTypeEx.
+From Coq Require Import Equalities Eqdep_dec FMapInterface.
 
 Require Import Lib.CommonTactics Lib.StringAsOT Lib.StringEq Lib.Struct.
 

Kami/Lib/N_Z_nat_conversions.v

@@ -1,5 +1,5 @@
 (* This should be in the Coq library *)
-Require Import Coq.Arith.Arith Coq.NArith.NArith Coq.ZArith.ZArith Lia.
+From Coq Require Import Arith NArith ZArith Lia.
 
 Lemma N_to_Z_to_nat: forall (a: N), Z.to_nat (Z.of_N a) = N.to_nat a.
 Proof.

Kami/Lib/NatLib.v

@@ -1,5 +1,5 @@
-Require Import Coq.NArith.NArith.
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import NArith.
+From Coq Require Import ZArith.
 Require Import N_Z_nat_conversions.
 Require Export Lia Nlia.
 

Kami/Lib/StringAsList.v

@@ -1,4 +1,4 @@
-Require Import String Program.Equality Lia.
+From Coq Require Import String Equality Lia.
 
 Set Asymmetric Patterns.
 

Kami/Lib/StringAsOT.v

@@ -1,5 +1,5 @@
-Require Import PeanoNat Compare_dec Lia Coq.Strings.String Coq.Strings.Ascii.
-Require Import Coq.Structures.OrderedType.
+From Coq Require Import PeanoNat Compare_dec Lia String Ascii.
+From Coq Require Import OrderedType.
 
 Set Asymmetric Patterns.
 

Kami/Lib/StringStringAsOT.v

@@ -1,4 +1,5 @@
-Require Import Coq.Structures.OrderedType String Lib.StringAsOT.
+From Coq Require Import OrderedType String.
+Require Import Lib.StringAsOT.
 
 Module StringString_as_OT <: OrderedType.
   Definition t := (string * string)%type.

Kami/Lib/Word.v

@@ -2,7 +2,7 @@
 
 Require Import Arith NArith ZArith Bool Lia.
 Require Import Eqdep_dec EqdepFacts.
-Require Import Program.Tactics Program.Equality.
+From Coq.Program Require Import Tactics Equality.
 Require Import Ring Ring_polynom.
 Require Import Lia Nlia NatLib DepEq N_Z_nat_conversions.
 

Kami/Lib/ilist.v

@@ -3,11 +3,11 @@ Set Implicit Arguments.
 
 Set Asymmetric Patterns.
 
-Require Import Coq.Lists.List
-        Coq.Strings.String
-        Coq.Arith.Arith Program.Equality.
+From Coq Require Import List
+        String
+        Arith Equality.
 Require Export Lib.VectorFacts.
-Require Coq.Vectors.Vector.
+From Coq Require Vector.
 
 Set Universe Polymorphism.
 Section ilist.

Kami/ModuleBound.v

@@ -1,4 +1,4 @@
-Require Import Bool String List Arith.Peano_dec.
+From Coq Require Import Bool String List Peano_dec.
 Require Import Lib.FMap Lib.Struct Lib.CommonTactics Lib.Concat Lib.Indexer Lib.StringEq.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts.
 Require Import Kami.Specialize Kami.Duplicate.

Kami/ModuleBoundEx.v

@@ -1,4 +1,4 @@
-Require Import Bool String List Arith.Peano_dec.
+Require Import Bool String List Peano_dec.
 Require Import Lib.FMap Lib.Struct Lib.CommonTactics Lib.Concat Lib.Indexer Lib.StringEq.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.RefinementFacts.
 Require Import Kami.Specialize Kami.Duplicate Kami.Notations.

Kami/PartialInlineFacts.v

@@ -1,8 +1,8 @@
-Require Import Bool List String.
+From Coq Require Import Bool List String.
 Require Import Lib.CommonTactics Lib.Struct.
 Require Import Lib.ilist Lib.Word Lib.FMap Lib.StringEq Lib.ListSupport.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.RefinementFacts Kami.Wf Kami.Inline Kami.InlineFacts.
-Require Import Program.Equality FunctionalExtensionality.
+From Coq Require Import Equality FunctionalExtensionality.
 
 Import ListNotations.
 

Kami/PrimBram.v

@@ -1,4 +1,4 @@
-Require Import Arith.Peano_dec Bool String List.
+Require Import Peano_dec Bool String List.
 Require Import Lib.Word Lib.Indexer.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics.
 Require Import Kami.Wf Kami.Tactics.

Kami/PrimFifo.v

@@ -1,4 +1,4 @@
-Require Import Arith.Peano_dec Bool String List.
+Require Import Peano_dec Bool String List.
 Require Import Lib.Indexer.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics.
 Require Import Kami.Wf Kami.Tactics.

Kami/RefinementFacts.v

@@ -1,5 +1,5 @@
-Require Import Bool List String Lia.
-Require Import Program.Equality Program.Basics Classes.Morphisms.
+From Coq Require Import Bool List String Lia.
+From Coq Require Import Equality Basics Morphisms.
 Require Import Lib.CommonTactics Lib.Indexer Lib.FMap Lib.Struct Lib.StringEq Lib.ListSupport.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.ModularFacts Kami.Wf.
 Require Import FunctionalExtensionality.

Kami/Renaming.v

@@ -1,5 +1,5 @@
 Require Import Lib.FMap Lib.Struct Kami.Semantics Kami.Syntax String List Kami.RefinementFacts.
-Require Import Program.Equality.
+From Coq Require Import Equality.
 
 Require Import Lib.CommonTactics.
 

Kami/SemFacts.v

@@ -1,5 +1,5 @@
-Require Import Bool String List Program.Equality Program.Basics.
-Require Import FunctionalExtensionality Classes.Morphisms.
+From Coq Require Import Bool String List Equality Basics.
+From Coq Require Import FunctionalExtensionality Morphisms.
 Require Import Lib.CommonTactics Lib.FMap Lib.Struct Lib.StringEq.
 Require Import Kami.Syntax Kami.Semantics Kami.Wf.
 

Kami/Semantics.v

@@ -1,6 +1,6 @@
-Require Import Bool List String Lia.
-Require Import Structures.Equalities Program.Equality Eqdep Eqdep_dec.
-Require Import FunctionalExtensionality.
+From Coq Require Import Bool List String Lia.
+From Coq Require Import Equalities Equality Eqdep Eqdep_dec.
+From Coq Require Import FunctionalExtensionality.
 Require Import Lib.Word Lib.CommonTactics Lib.ilist Lib.FMap Lib.StringEq Lib.VectorFacts Lib.Struct.
 Require Import Kami.Syntax.
 

Kami/Specialize.v

@@ -1,9 +1,9 @@
-Require Import Bool String List Arith.Peano_dec Lia.
+From Coq Require Import Bool String List Peano_dec Lia.
 Require Import Lib.FMap Lib.Struct Lib.CommonTactics Lib.Indexer Lib.StringAsList Lib.StringEq.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.RefinementFacts Kami.Renaming Kami.Wf.
 
-Require Import FunctionalExtensionality.
-Require Import Compare_dec.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import Compare_dec.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.

Kami/Tactics.v

@@ -6,7 +6,7 @@ Require Import Kami.RefinementFacts Kami.Notations.
 Require Import Kami.Inline Kami.InlineFacts Kami.Specialize Kami.Duplicate Kami.Substitute.
 Require Import Kami.Decomposition Kami.ModuleBound Kami.ModuleBoundEx.
 
-Require Import FunctionalExtensionality Program.Equality.
+From Coq Require Import FunctionalExtensionality Equality.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.

Kami/Wf.v

@@ -1,8 +1,8 @@
-Require Import Bool List String Structures.Equalities.
+From Coq Require Import Bool List String Equalities.
 Require Import Lib.Struct Lib.Word Lib.CommonTactics.
 Require Import Lib.ilist Lib.FMap Lib.StringEq.
 Require Import Kami.Syntax Kami.Semantics.
-Require Import FunctionalExtensionality Program.Equality Eqdep Eqdep_dec.
+From Coq Require Import FunctionalExtensionality Equality Eqdep Eqdep_dec.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.