absolutize some imports

Kami/Ex/Btb.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.

Kami/Ex/Divider32.v

@@ -1,4 +1,4 @@
-Require Import Bool String List Lia.
+From Coq Require Import Bool String List Lia.
 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.

Kami/Ex/Divider64.v

@@ -1,9 +1,9 @@
-Require Import Bool String List Lia.
+From Coq Require Import Bool String List Lia.
 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 Equality.
+From Coq Require Import ZArith Eqdep Equality.
 
 Set Implicit Arguments.
 

Kami/Ex/Fifo.v

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

Kami/Ex/FifoCorrect.v

@@ -1,4 +1,4 @@
-Require Import Peano_dec Bool String List PeanoNat.
+From Coq 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/PgmBankerInit.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmBankerWorker1.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmBankerWorker2.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmBankerWorker3.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmBsort.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmDekker1.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmDekker2.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmFact.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmGcd.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmHanoi.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmMatMulInit.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmMatMulNormal1.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmMatMulNormal2.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmMatMulReport.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmPeterson1.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32/PgmPeterson2.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.Word Lib.Struct.
 Require Import Kami.Syntax.
 Require Import Ex.IsaRv32 Ex.IsaRv32Pgm.

Kami/Ex/IsaRv32Pgm.v

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

Kami/Ex/MemAsync.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.FMap Lib.Struct Lib.Reflection Lib.ilist Lib.Word Lib.Indexer.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics Kami.Specialize Kami.Duplicate Kami.RefinementFacts.
 Require Import Kami.SemFacts Kami.Wf Kami.Tactics.

Kami/Ex/MemTypes.v

@@ -1,4 +1,5 @@
-Require Import Kami.Syntax Kami.Notations String.
+From Coq Require Import String.
+Require Import Kami.Syntax Kami.Notations.
 Require Import Names.
 
 Definition MemOp := Bool.

Kami/Ex/Multiplier32.v

@@ -1,4 +1,4 @@
-Require Import Bool String List Lia.
+From Coq Require Import Bool String List Lia.
 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.

Kami/Ex/Multiplier64.v

@@ -1,9 +1,9 @@
-Require Import Bool String List Lia.
+From Coq Require Import Bool String List Lia.
 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 Equality.
+From Coq Require Import ZArith Eqdep Equality.
 
 Set Implicit Arguments.
 Open Scope string.

Kami/Ex/Names.v

@@ -1,4 +1,4 @@
-Require Import String.
+From Coq Require Import String.
 
 Local Open Scope string.
 Definition procRqValidReg := "procRqValid".

Kami/Ex/NativeFifo.v

@@ -1,4 +1,4 @@
-Require Import Peano_dec Bool String List.
+From Coq 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/OneEltFifo.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word Lib.Indexer.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics Kami.Wf Kami.Tactics.
 

Kami/Ex/ProcDec.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word Lib.Indexer.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics Kami.Specialize Kami.Duplicate.
 Require Import Kami.Wf Kami.Tactics.

Kami/Ex/ProcDecInv.v

@@ -1,4 +1,4 @@
-Require Import Bool String List BinNums Lia.
+From Coq Require Import Bool String List BinNums Lia.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.

Kami/Ex/ProcDecSC.v

@@ -1,4 +1,4 @@
-Require Import Bool String List Lia.
+From Coq Require Import Bool String List Lia.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.

Kami/Ex/ProcDecSCN.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts.

Kami/Ex/ProcFCorrect.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.

Kami/Ex/ProcFDCorrect.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.

Kami/Ex/ProcFDInl.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.
 Require Import Kami.Inline Kami.InlineFacts Kami.Tactics.
 Require Import Ex.SC Ex.MemTypes Ex.ProcFetchDecode.

Kami/Ex/ProcFDInv.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.

Kami/Ex/ProcFInl.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.
 Require Import Kami.Inline Kami.InlineFacts Kami.Tactics.
 Require Import Ex.SC Ex.MemTypes Ex.ProcFetch.

Kami/Ex/ProcFInv.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.

Kami/Ex/ProcFetch.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word Lib.Indexer.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics Kami.Specialize Kami.Duplicate.
 Require Import Kami.Wf Kami.Tactics.

Kami/Ex/ProcFetchDecode.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word Lib.Indexer.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics Kami.Specialize Kami.Duplicate.
 Require Import Kami.Wf Kami.Tactics.

Kami/Ex/ProcFourStDec.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.

Kami/Ex/ProcMemCorrect.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.

Kami/Ex/ProcThreeStDec.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.

Kami/Ex/ProcThreeStInv.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word.
 Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
 Require Import Kami.Syntax Kami.Semantics Kami.RefinementFacts Kami.Renaming Kami.Wf.

Kami/Ex/ProcThreeStage.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics Lib.ilist Lib.Word Lib.Indexer.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics Kami.Specialize Kami.Duplicate.
 Require Import Kami.Wf Kami.Tactics.

Kami/Ex/RegFile.v

@@ -1,4 +1,5 @@
-Require Import String Lib.CommonTactics Lib.Indexer Lib.StringAsList.
+From Coq Require Import String.
+Require Import Lib.CommonTactics Lib.Indexer Lib.StringAsList.
 Require Import Kami.Syntax Kami.Notations Kami.Semantics.
 Require Import Kami.Wf Kami.Tactics.
 

Kami/Ex/SC.v

@@ -1,4 +1,4 @@
-Require Import Ascii Bool String List Lia.
+From Coq Require Import Ascii Bool String List Lia.
 Require Import Lib.CommonTactics Lib.Indexer Lib.ilist Lib.Word Lib.Struct.
 Require Import Kami.Syntax Kami.Notations.
 Require Import Kami.Semantics Kami.Specialize Kami.Duplicate.

Kami/Ex/SCMMInl.v

@@ -1,4 +1,4 @@
-Require Import Ascii Bool String List.
+From Coq Require Import Ascii Bool String List.
 Require Import Lib.CommonTactics Lib.Indexer Lib.ilist Lib.Word Lib.Struct.
 Require Import Kami.Syntax Kami.Notations.
 Require Import Kami.Semantics Kami.Specialize Kami.Duplicate.

Kami/Ex/SCMMInv.v

@@ -1,4 +1,4 @@
-Require Import Ascii Bool String List Lia.
+From Coq Require Import Ascii Bool String List Lia.
 Require Import Lib.CommonTactics Lib.Indexer Lib.ilist Lib.Word Lib.Struct Lib.FMap.
 Require Import Kami.Syntax Kami.Notations.
 Require Import Kami.Semantics Kami.Specialize Kami.Duplicate.

Kami/Ex/SimpleFifoCorrect.v

@@ -1,4 +1,4 @@
-Require Import Peano_dec Bool String List PeanoNat.
+From Coq 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/Ext/BSyntax.v

@@ -1,4 +1,4 @@
-Require Import String List.
+From Coq Require Import String List.
 Require Import Lib.Word Lib.ilist Lib.Struct Lib.Indexer.
 Require Import Kami.Syntax Kami.Synthesize.
 

Kami/Inline.v

@@ -1,4 +1,4 @@
-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.
 Require Import Kami.Syntax.

Kami/InlineFacts.v

@@ -1,4 +1,4 @@
-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.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts.

Kami/Kami.v

@@ -1,4 +1,4 @@
-Require Export Bool String List.
+From Coq Require Export Bool String List.
 
 Require Export Lib.CommonTactics Lib.Indexer.
 Require Export Lib.FMap Lib.Word Lib.Struct.

Kami/Label.v

@@ -1,4 +1,4 @@
-Require Import Bool List String.
+From Coq Require Import Bool List String.
 Require Import Lib.CommonTactics Lib.FMap.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts.
 

Kami/Lib/Concat.v

@@ -1,4 +1,4 @@
-Require Import List String.
+From Coq Require Import List String.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.

Kami/Lib/Indexer.v

@@ -1,4 +1,4 @@
-Require Import Bool Ascii String Eqdep PeanoNat Compare_dec Lia.
+From Coq Require Import Bool Ascii String Eqdep PeanoNat Compare_dec Lia.
 Require Import CommonTactics StringAsList StringEq.
 
 (** Some string manipulation lemmas *)

Kami/Lib/Misc.v

@@ -1,4 +1,5 @@
-Require Import String StringAsList.
+From Coq Require Import String.
+Require Import StringAsList.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.

Kami/Lib/Nlia.v

@@ -1,6 +1,6 @@
 (* Make [lia] work for [N] *)
 
-Require Import Arith Lia NArith.
+From Coq Require Import Arith Lia NArith.
 
 Local Open Scope N_scope.
 

Kami/Lib/Reflection.v

@@ -1,4 +1,4 @@
-Require Import Bool String List.
+From Coq Require Import Bool String List.
 Require Import Lib.CommonTactics.
 
 Set Implicit Arguments.

Kami/Lib/StringEq.v

@@ -1,4 +1,4 @@
-Require Import Bool Ascii String List.
+From Coq Require Import Bool Ascii String List.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.

Kami/Lib/Struct.v

@@ -1,5 +1,6 @@
-Require Import String Lib.Word List Arith.
-Require Import Equality Eqdep_dec FunctionalExtensionality.
+From Coq Require Import String List Arith.
+Require Import Lib.Word.
+From Coq Require Import Equality Eqdep_dec FunctionalExtensionality.
 Require Import Lib.CommonTactics Lib.StringEq.
 
 Set Implicit Arguments.