diff --git a/Kami/Ex/Btb.v b/Kami/Ex/Btb.v
index a88da037..6044f000 100644
--- a/Kami/Ex/Btb.v
+++ b/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.
diff --git a/Kami/Ex/Divider32.v b/Kami/Ex/Divider32.v
index c64ca977..8a00f95b 100644
--- a/Kami/Ex/Divider32.v
+++ b/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.
diff --git a/Kami/Ex/Divider64.v b/Kami/Ex/Divider64.v
index 9dfd9270..13d15eb7 100644
--- a/Kami/Ex/Divider64.v
+++ b/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.
 
diff --git a/Kami/Ex/Fifo.v b/Kami/Ex/Fifo.v
index 37a2bc01..039003b7 100644
--- a/Kami/Ex/Fifo.v
+++ b/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.
diff --git a/Kami/Ex/FifoCorrect.v b/Kami/Ex/FifoCorrect.v
index e35c1b23..3d49fca4 100644
--- a/Kami/Ex/FifoCorrect.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmBankerInit.v b/Kami/Ex/IsaRv32/PgmBankerInit.v
index 54ae7fff..8b24a1bd 100644
--- a/Kami/Ex/IsaRv32/PgmBankerInit.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmBankerWorker1.v b/Kami/Ex/IsaRv32/PgmBankerWorker1.v
index 1c4fd34b..e0245409 100644
--- a/Kami/Ex/IsaRv32/PgmBankerWorker1.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmBankerWorker2.v b/Kami/Ex/IsaRv32/PgmBankerWorker2.v
index de98aff8..89625ab4 100644
--- a/Kami/Ex/IsaRv32/PgmBankerWorker2.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmBankerWorker3.v b/Kami/Ex/IsaRv32/PgmBankerWorker3.v
index 84b67ec2..77660e2f 100644
--- a/Kami/Ex/IsaRv32/PgmBankerWorker3.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmBsort.v b/Kami/Ex/IsaRv32/PgmBsort.v
index 848c7470..bbf761ea 100644
--- a/Kami/Ex/IsaRv32/PgmBsort.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmDekker1.v b/Kami/Ex/IsaRv32/PgmDekker1.v
index 540f3377..bb2535ef 100644
--- a/Kami/Ex/IsaRv32/PgmDekker1.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmDekker2.v b/Kami/Ex/IsaRv32/PgmDekker2.v
index cbc676c7..5527c35e 100644
--- a/Kami/Ex/IsaRv32/PgmDekker2.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmFact.v b/Kami/Ex/IsaRv32/PgmFact.v
index e243c6ed..d5984288 100644
--- a/Kami/Ex/IsaRv32/PgmFact.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmGcd.v b/Kami/Ex/IsaRv32/PgmGcd.v
index 4fb0f101..fe694fc2 100644
--- a/Kami/Ex/IsaRv32/PgmGcd.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmHanoi.v b/Kami/Ex/IsaRv32/PgmHanoi.v
index 5f499672..04e7604d 100644
--- a/Kami/Ex/IsaRv32/PgmHanoi.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmMatMulInit.v b/Kami/Ex/IsaRv32/PgmMatMulInit.v
index 08dd807b..a3dacf5d 100644
--- a/Kami/Ex/IsaRv32/PgmMatMulInit.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmMatMulNormal1.v b/Kami/Ex/IsaRv32/PgmMatMulNormal1.v
index 4e9760ee..5b9e5045 100644
--- a/Kami/Ex/IsaRv32/PgmMatMulNormal1.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmMatMulNormal2.v b/Kami/Ex/IsaRv32/PgmMatMulNormal2.v
index 7bfc8ad6..103d1454 100644
--- a/Kami/Ex/IsaRv32/PgmMatMulNormal2.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmMatMulReport.v b/Kami/Ex/IsaRv32/PgmMatMulReport.v
index 3618f291..ebf8d9a7 100644
--- a/Kami/Ex/IsaRv32/PgmMatMulReport.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmPeterson1.v b/Kami/Ex/IsaRv32/PgmPeterson1.v
index 624bb498..01944d66 100644
--- a/Kami/Ex/IsaRv32/PgmPeterson1.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32/PgmPeterson2.v b/Kami/Ex/IsaRv32/PgmPeterson2.v
index 25f5f66d..97f03167 100644
--- a/Kami/Ex/IsaRv32/PgmPeterson2.v
+++ b/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.
diff --git a/Kami/Ex/IsaRv32Pgm.v b/Kami/Ex/IsaRv32Pgm.v
index 420ae854..5a4a9d66 100644
--- a/Kami/Ex/IsaRv32Pgm.v
+++ b/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.
diff --git a/Kami/Ex/MemAsync.v b/Kami/Ex/MemAsync.v
index 334323ac..e8198d85 100644
--- a/Kami/Ex/MemAsync.v
+++ b/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.
diff --git a/Kami/Ex/MemTypes.v b/Kami/Ex/MemTypes.v
index 6cc9d140..45ae898e 100644
--- a/Kami/Ex/MemTypes.v
+++ b/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.
diff --git a/Kami/Ex/Multiplier32.v b/Kami/Ex/Multiplier32.v
index 6e456f99..dcf12330 100644
--- a/Kami/Ex/Multiplier32.v
+++ b/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.
diff --git a/Kami/Ex/Multiplier64.v b/Kami/Ex/Multiplier64.v
index 2f05e886..f8412cd3 100644
--- a/Kami/Ex/Multiplier64.v
+++ b/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.
diff --git a/Kami/Ex/Names.v b/Kami/Ex/Names.v
index b96fd3ce..786d5cad 100644
--- a/Kami/Ex/Names.v
+++ b/Kami/Ex/Names.v
@@ -1,4 +1,4 @@
-Require Import String.
+From Coq Require Import String.
 
 Local Open Scope string.
 Definition procRqValidReg := "procRqValid".
diff --git a/Kami/Ex/NativeFifo.v b/Kami/Ex/NativeFifo.v
index baad23a6..9ad65e81 100644
--- a/Kami/Ex/NativeFifo.v
+++ b/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.
diff --git a/Kami/Ex/OneEltFifo.v b/Kami/Ex/OneEltFifo.v
index d782ca12..2f5bf17a 100644
--- a/Kami/Ex/OneEltFifo.v
+++ b/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.
 
diff --git a/Kami/Ex/ProcDec.v b/Kami/Ex/ProcDec.v
index 65df6bec..4e7e142c 100644
--- a/Kami/Ex/ProcDec.v
+++ b/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.
diff --git a/Kami/Ex/ProcDecInv.v b/Kami/Ex/ProcDecInv.v
index bf2e2418..a0b6f7f5 100644
--- a/Kami/Ex/ProcDecInv.v
+++ b/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.
diff --git a/Kami/Ex/ProcDecSC.v b/Kami/Ex/ProcDecSC.v
index 8b7a2c1a..6ff06843 100644
--- a/Kami/Ex/ProcDecSC.v
+++ b/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.
diff --git a/Kami/Ex/ProcDecSCN.v b/Kami/Ex/ProcDecSCN.v
index 7fd7d420..9c530d77 100644
--- a/Kami/Ex/ProcDecSCN.v
+++ b/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.
diff --git a/Kami/Ex/ProcFCorrect.v b/Kami/Ex/ProcFCorrect.v
index 8714717a..d367e100 100644
--- a/Kami/Ex/ProcFCorrect.v
+++ b/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.
diff --git a/Kami/Ex/ProcFDCorrect.v b/Kami/Ex/ProcFDCorrect.v
index 08b393cf..58b1647a 100644
--- a/Kami/Ex/ProcFDCorrect.v
+++ b/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.
diff --git a/Kami/Ex/ProcFDInl.v b/Kami/Ex/ProcFDInl.v
index d6cd455f..668f7d22 100644
--- a/Kami/Ex/ProcFDInl.v
+++ b/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.
diff --git a/Kami/Ex/ProcFDInv.v b/Kami/Ex/ProcFDInv.v
index f85d9cd0..8d67148b 100644
--- a/Kami/Ex/ProcFDInv.v
+++ b/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.
diff --git a/Kami/Ex/ProcFInl.v b/Kami/Ex/ProcFInl.v
index 0740d87f..07c644b0 100644
--- a/Kami/Ex/ProcFInl.v
+++ b/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.
diff --git a/Kami/Ex/ProcFInv.v b/Kami/Ex/ProcFInv.v
index 43c64808..9c814884 100644
--- a/Kami/Ex/ProcFInv.v
+++ b/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.
diff --git a/Kami/Ex/ProcFetch.v b/Kami/Ex/ProcFetch.v
index eaf4d93f..285a88f4 100644
--- a/Kami/Ex/ProcFetch.v
+++ b/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.
diff --git a/Kami/Ex/ProcFetchDecode.v b/Kami/Ex/ProcFetchDecode.v
index a265bf28..a66b2fc3 100644
--- a/Kami/Ex/ProcFetchDecode.v
+++ b/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.
diff --git a/Kami/Ex/ProcFourStDec.v b/Kami/Ex/ProcFourStDec.v
index 74e99c0c..4f1c30fa 100644
--- a/Kami/Ex/ProcFourStDec.v
+++ b/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.
diff --git a/Kami/Ex/ProcMemCorrect.v b/Kami/Ex/ProcMemCorrect.v
index 2f460eff..7b226318 100644
--- a/Kami/Ex/ProcMemCorrect.v
+++ b/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.
diff --git a/Kami/Ex/ProcThreeStDec.v b/Kami/Ex/ProcThreeStDec.v
index 22d9ce30..3e725960 100644
--- a/Kami/Ex/ProcThreeStDec.v
+++ b/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.
diff --git a/Kami/Ex/ProcThreeStInv.v b/Kami/Ex/ProcThreeStInv.v
index 0b399cbb..4976f5bf 100644
--- a/Kami/Ex/ProcThreeStInv.v
+++ b/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.
diff --git a/Kami/Ex/ProcThreeStage.v b/Kami/Ex/ProcThreeStage.v
index 3746afd4..04195701 100644
--- a/Kami/Ex/ProcThreeStage.v
+++ b/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.
diff --git a/Kami/Ex/RegFile.v b/Kami/Ex/RegFile.v
index 9733c0f1..985e3f44 100644
--- a/Kami/Ex/RegFile.v
+++ b/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.
 
diff --git a/Kami/Ex/SC.v b/Kami/Ex/SC.v
index 6833482c..8ecc5f13 100644
--- a/Kami/Ex/SC.v
+++ b/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.
diff --git a/Kami/Ex/SCMMInl.v b/Kami/Ex/SCMMInl.v
index 1b6dc830..3d7bbd15 100644
--- a/Kami/Ex/SCMMInl.v
+++ b/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.
diff --git a/Kami/Ex/SCMMInv.v b/Kami/Ex/SCMMInv.v
index cb0a398a..86355bf6 100644
--- a/Kami/Ex/SCMMInv.v
+++ b/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.
diff --git a/Kami/Ex/SimpleFifoCorrect.v b/Kami/Ex/SimpleFifoCorrect.v
index fda581b2..e4245634 100644
--- a/Kami/Ex/SimpleFifoCorrect.v
+++ b/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.
diff --git a/Kami/Ext/BSyntax.v b/Kami/Ext/BSyntax.v
index f9b6ad6a..13c2362a 100644
--- a/Kami/Ext/BSyntax.v
+++ b/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.
 
diff --git a/Kami/Inline.v b/Kami/Inline.v
index 04c2a877..e0a60489 100644
--- a/Kami/Inline.v
+++ b/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.
diff --git a/Kami/InlineFacts.v b/Kami/InlineFacts.v
index d8ad642b..458cd99f 100644
--- a/Kami/InlineFacts.v
+++ b/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.
diff --git a/Kami/Kami.v b/Kami/Kami.v
index b7321d81..6212105f 100644
--- a/Kami/Kami.v
+++ b/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.
diff --git a/Kami/Label.v b/Kami/Label.v
index 54da9fb5..9b857193 100644
--- a/Kami/Label.v
+++ b/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.
 
diff --git a/Kami/Lib/Concat.v b/Kami/Lib/Concat.v
index 95f81bc1..74564640 100644
--- a/Kami/Lib/Concat.v
+++ b/Kami/Lib/Concat.v
@@ -1,4 +1,4 @@
-Require Import List String.
+From Coq Require Import List String.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
diff --git a/Kami/Lib/Indexer.v b/Kami/Lib/Indexer.v
index 06bae422..296c7577 100644
--- a/Kami/Lib/Indexer.v
+++ b/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 *)
diff --git a/Kami/Lib/Misc.v b/Kami/Lib/Misc.v
index 42f82e8a..c8da272b 100644
--- a/Kami/Lib/Misc.v
+++ b/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.
diff --git a/Kami/Lib/Nlia.v b/Kami/Lib/Nlia.v
index c3986a54..13658c11 100644
--- a/Kami/Lib/Nlia.v
+++ b/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.
 
diff --git a/Kami/Lib/Reflection.v b/Kami/Lib/Reflection.v
index d01bbe62..51b30034 100644
--- a/Kami/Lib/Reflection.v
+++ b/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.
diff --git a/Kami/Lib/StringEq.v b/Kami/Lib/StringEq.v
index 81b2359d..09374555 100644
--- a/Kami/Lib/StringEq.v
+++ b/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.
diff --git a/Kami/Lib/Struct.v b/Kami/Lib/Struct.v
index 7d0c802f..b4dc841a 100644
--- a/Kami/Lib/Struct.v
+++ b/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.
diff --git a/Kami/Lib/Word.v b/Kami/Lib/Word.v
index 50a58754..e68207ab 100644
--- a/Kami/Lib/Word.v
+++ b/Kami/Lib/Word.v
@@ -1,10 +1,10 @@
 (** Fixed precision machine words *)
 
-Require Import Arith NArith ZArith Bool Lia.
-Require Import Eqdep_dec EqdepFacts.
+From Coq Require Import Arith NArith ZArith Bool Lia.
+From Coq Require Import Eqdep_dec EqdepFacts.
 From Coq.Program Require Import Tactics Equality.
-Require Import Ring Ring_polynom.
-Require Import Lia Nlia NatLib DepEq N_Z_nat_conversions.
+From Coq Require Import Ring Ring_polynom Lia.
+From Kami Require Import Nlia NatLib DepEq N_Z_nat_conversions.
 
 Set Implicit Arguments.
 
diff --git a/Kami/ModularFacts.v b/Kami/ModularFacts.v
index 9c8fd421..f6b941c4 100644
--- a/Kami/ModularFacts.v
+++ b/Kami/ModularFacts.v
@@ -1,4 +1,4 @@
-Require Import List String.
+From Coq Require Import List String.
 Require Import Lib.CommonTactics Lib.Struct Lib.FMap.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.Wf.
 
diff --git a/Kami/ModuleBoundEx.v b/Kami/ModuleBoundEx.v
index 5a929ebe..58073c9c 100644
--- a/Kami/ModuleBoundEx.v
+++ b/Kami/ModuleBoundEx.v
@@ -1,4 +1,4 @@
-Require Import Bool String List 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 Kami.RefinementFacts.
 Require Import Kami.Specialize Kami.Duplicate Kami.Notations.
diff --git a/Kami/Notations.v b/Kami/Notations.v
index f06d22b6..bf86a914 100644
--- a/Kami/Notations.v
+++ b/Kami/Notations.v
@@ -1,4 +1,4 @@
-Require Import Bool List String.
+From Coq Require Import Bool List String.
 Require Import Lib.Struct Lib.Word Lib.ilist Lib.Indexer Lib.StringAsList.
 Require Import Kami.Syntax.
 
diff --git a/Kami/PrimBram.v b/Kami/PrimBram.v
index e7b12913..5554c53b 100644
--- a/Kami/PrimBram.v
+++ b/Kami/PrimBram.v
@@ -1,4 +1,4 @@
-Require Import Peano_dec Bool String List.
+From Coq 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.
diff --git a/Kami/PrimFifo.v b/Kami/PrimFifo.v
index 36a2fac2..1db2c525 100644
--- a/Kami/PrimFifo.v
+++ b/Kami/PrimFifo.v
@@ -1,4 +1,4 @@
-Require Import Peano_dec Bool String List.
+From Coq 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.
diff --git a/Kami/Renaming.v b/Kami/Renaming.v
index 347a6a6d..822008c8 100644
--- a/Kami/Renaming.v
+++ b/Kami/Renaming.v
@@ -1,5 +1,5 @@
-Require Import Lib.FMap Lib.Struct Kami.Semantics Kami.Syntax String List Kami.RefinementFacts.
-From Coq Require Import Equality.
+Require Import Lib.FMap Lib.Struct Kami.Semantics Kami.Syntax Kami.RefinementFacts.
+From Coq Require Import String List Equality.
 
 Require Import Lib.CommonTactics.
 
diff --git a/Kami/StepDet.v b/Kami/StepDet.v
index 4567b07d..6218ca31 100644
--- a/Kami/StepDet.v
+++ b/Kami/StepDet.v
@@ -1,4 +1,4 @@
-Require Import Bool List String Lia.
+From Coq Require Import Bool List String Lia.
 Require Import Lib.CommonTactics Lib.Struct Lib.Reflection Lib.FMap Lib.Struct Lib.StringEq.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.Wf.
 
diff --git a/Kami/Substitute.v b/Kami/Substitute.v
index cbf23b25..bca265ee 100644
--- a/Kami/Substitute.v
+++ b/Kami/Substitute.v
@@ -1,4 +1,4 @@
-Require Import List String.
+From Coq Require Import List String.
 Require Import Lib.CommonTactics Lib.FMap Lib.Struct.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.RefinementFacts Kami.Wf.
 
diff --git a/Kami/Syntax.v b/Kami/Syntax.v
index 9bac3a2e..5d4e6929 100644
--- a/Kami/Syntax.v
+++ b/Kami/Syntax.v
@@ -1,4 +1,4 @@
-Require Import Bool Peano_dec Vector List String.
+From Coq Require Import Bool Peano_dec Vector List String.
 Require Import Lib.CommonTactics Lib.StringEq Lib.Word Lib.FMap Lib.StringEq Lib.ilist Lib.Struct Lib.Indexer.
 
 Require Import FunctionalExtensionality. (* for appendAction_assoc *)
diff --git a/Kami/Synthesize.v b/Kami/Synthesize.v
index 2eea90d5..3f4b0815 100644
--- a/Kami/Synthesize.v
+++ b/Kami/Synthesize.v
@@ -1,4 +1,5 @@
-Require Import Kami.Syntax Lib.Struct List String Kami.Notations.
+From Coq Require Import List String.
+Require Import Kami.Syntax Lib.Struct Kami.Notations.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
diff --git a/Kami/Tactics.v b/Kami/Tactics.v
index 0c37e010..43276d17 100644
--- a/Kami/Tactics.v
+++ b/Kami/Tactics.v
@@ -1,4 +1,4 @@
-Require Import Bool String List Eqdep.
+From Coq Require Import Bool String List Eqdep.
 Require Import Lib.CommonTactics Lib.Reflection Lib.Word Lib.ilist Lib.Struct.
 Require Import Lib.Indexer Lib.StringEq Lib.FMap.
 Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.StepDet Kami.Wf.