saw-core-coq: Coq => Stdlib in qualified names.

Author: chathhorn-galois

saw-core-coq/coq/handwritten/CryptolToCoq/CoqVectorsExtra.v

@@ -1,4 +1,4 @@
-(* This file contains definitions that seemed missing from Coq.Vectors.Vector *)
+(* This file contains definitions that seemed missing from Stdlib.Vectors.Vector *)
 
 From Stdlib         Require Import PeanoNat.
 From Stdlib.Vectors Require Vector.

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v

@@ -102,7 +102,7 @@ Definition or     := orb.
 (** DEPRECATED: Use [xorb] instead. *)
 Definition xor    := xorb.
 
-Definition boolEq := Coq.Bool.Bool.eqb.
+Definition boolEq := Stdlib.Bool.Bool.eqb.
 
 Global Instance Inhabited_Unit : Inhabited UnitType :=
   MkInhabited UnitType tt.

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffoldingCopy.v

@@ -34,7 +34,7 @@ Preprocess Module SCS as SCS'.
   Definition not      := negb.
   Definition or     := orb.
   Definition xor    := xorb.
-  Definition boolEq := Coq.Bool.Bool.eqb.
+  Definition boolEq := Stdlib.Bool.Bool.eqb.
   Theorem boolEq__eq (b1 b2:Bool) : Eq Bool (boolEq b1 b2) (ite Bool b1 b2 (not b2)).
   Proof.
     destruct b1, b2; reflexivity.

saw-core-coq/src/SAWCoreCoq/SpecialTreatment.hs

@@ -175,32 +175,32 @@ skip = IdentSpecialTreatment
 -- | The Coq built-in @Datatypes@ module
 datatypesModule :: ModuleName
 datatypesModule =
-  mkModuleName ["Coq", "Init", "Datatypes"]
+  mkModuleName ["Init", "Datatypes"]
 
 -- | The Coq built-in @Logic@ module
 logicModule :: ModuleName
 logicModule =
-  mkModuleName ["Coq", "Init", "Logic"]
+  mkModuleName ["Init", "Logic"]
 
 -- | The Coq built-in @String@ module.
 stringModule :: ModuleName
 stringModule =
-  mkModuleName ["Coq", "Strings", "String"]
+  mkModuleName ["Stdlib", "Strings", "String"]
 
 -- | The Coq built-in @BinNums@ module.
 binNumsModule :: ModuleName
 binNumsModule =
-  mkModuleName ["Coq", "Numbers", "BinNums"]
+  mkModuleName ["Stdlib", "Numbers", "BinNums"]
 
 -- | The Coq built-in @BinPos@ module.
 binPosModule :: ModuleName
 binPosModule =
-  mkModuleName ["Coq", "PArith", "BinPos"]
+  mkModuleName ["Stdlib", "PArith", "BinPos"]
 
 -- | The Coq built-in @BinInt@ module.
 binIntModule :: ModuleName
 binIntModule =
-  mkModuleName ["Coq", "ZArith", "BinInt"]
+  mkModuleName ["Stdlib", "ZArith", "BinInt"]
 
 -- | The @SAWCoreScaffolding@ module
 sawDefinitionsModule :: ModuleName