Merge pull request #1086 from GaloisInc/fix-coq-import-bug

fix coq import bug (SAWVector.. -> SAWCoreVector..)
GaloisInc · Feb 24, 2021 · e3a317a · e3a317a
2 parents 7b71012 + 919d605
commit e3a317a
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/deps/saw-core b/deps/saw-core
diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
@@ -280,7 +280,7 @@ coqTranslationConfiguration notations skips = Coq.TranslationConfiguration
   { Coq.notations          = notations
   , Coq.monadicTranslation = False
   , Coq.skipDefinitions    = skips
-  , Coq.vectorModule       = "SAWVectorsAsCoqVectors"
+  , Coq.vectorModule       = "SAWCoreVectorsAsCoqVectors"
   }
 
 writeCoqTerm ::
+74 −74		saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
+93 −93		saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
+4 −1		saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
+4 −2		saw-core/src/Verifier/SAW/ExternalFormat.hs
+12 −11		saw-core/src/Verifier/SAW/Grammar.y
+23 −22		saw-core/src/Verifier/SAW/Module.hs
+4 −0		saw-core/src/Verifier/SAW/Name.hs
+81 −8		saw-core/src/Verifier/SAW/OpenTerm.hs
+8 −6		saw-core/src/Verifier/SAW/ParserUtils.hs
+0 −18		saw-core/src/Verifier/SAW/Prelude/Constants.hs
+8 −2		saw-core/src/Verifier/SAW/Recognizer.hs
+8 −8		saw-core/src/Verifier/SAW/Rewriter.hs
+8 −9		saw-core/src/Verifier/SAW/SCTypeCheck.hs
+9 −12		saw-core/src/Verifier/SAW/SharedTerm.hs
+5 −1		saw-core/src/Verifier/SAW/Simulator.hs
+5 −3		saw-core/src/Verifier/SAW/Term/Functor.hs
+4 −4		saw-core/src/Verifier/SAW/Term/Pretty.hs
+20 −14		saw-core/src/Verifier/SAW/Typechecker.hs
+20 −18		saw-core/src/Verifier/SAW/UntypedAST.hs