Fix imports

AU-COBRA · Apr 11, 2023 · f0e8ea8 · f0e8ea8
1 parent 8afef8b
commit f0e8ea8
Show file tree

Hide file tree

Showing 6 changed files with 11 additions and 12 deletions.
diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked
@@ -65,6 +65,6 @@ pin-depends: [
   ]
   [
     "coq-rust-extraction.dev"
-    "git+https://github.com/AU-COBRA/coq-rust-extraction.git#22564dba4603bae51002b59c603e80f515758d77"
+    "git+https://github.com/AU-COBRA/coq-rust-extraction.git#11914d450868173dcde57fc11abc700bf55c8a0c"
   ]
 ]
diff --git a/coq-concert.opam b/coq-concert.opam
@@ -37,7 +37,7 @@ pin-depends: [
   ["coq-metacoq-pcuic.8.16.dev" "git+https://github.com/MetaCoq/metacoq.git#b96e7570a5e7fd959fe171d63398f4491fed338a"]
   ["coq-metacoq-safechecker.8.16.dev" "git+https://github.com/MetaCoq/metacoq.git#b96e7570a5e7fd959fe171d63398f4491fed338a"]
   ["coq-metacoq-erasure.8.16.dev" "git+https://github.com/MetaCoq/metacoq.git#b96e7570a5e7fd959fe171d63398f4491fed338a"]
-  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#22564dba4603bae51002b59c603e80f515758d77"]
+  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#11914d450868173dcde57fc11abc700bf55c8a0c"]
 ]
 
 build: [

diff --git a/examples/_CoqProject b/examples/_CoqProject
@@ -7,7 +7,6 @@
 -R ../embedding/theories ConCert.Embedding
 -R ../embedding/extraction ConCert.Embedding.Extraction
 -R ../extraction/theories ConCert.Extraction
--R ../extraction/plugin/theories ConCert.Extraction
 
 -Q eip20 ConCert.Examples.EIP20
 eip20/EIP20Token.v

diff --git a/examples/counter/extraction/CounterRust.v b/examples/counter/extraction/CounterRust.v
@@ -1,7 +1,7 @@
 From ConCert.Examples.Counter Require Counter.
 From ConCert.Extraction Require Import Common.
 From ConCert.Extraction Require Import ConcordiumExtract.
-From ConCert.Extraction Require Import RustExtract.
+From RustExtraction Require Import RustExtract.
 From Coq Require Import Bool.
 From Coq Require Import String.
 From MetaCoq.Template Require Import All.

diff --git a/examples/stackInterpreter/StackInterpreterRustExtract.v b/examples/stackInterpreter/StackInterpreterRustExtract.v
@@ -1,9 +1,9 @@
 From ConCert.Examples.StackInterpreter Require Import StackInterpreter.
-From ConCert.Extraction Require Import RustExtract.
+From RustExtraction Require Import RustExtract.
+From RustExtraction Require Import Printing.
 From ConCert.Extraction Require Import Common.
-From ConCert.Extraction Require Import Printing.
 From ConCert.Extraction Require Import ConcordiumExtract.
-From ConCert.Utils Require Import StringExtra.
+From RustExtraction Require Import StringExtra.
 From MetaCoq.Template Require Import All.
 From MetaCoq.TemplatePCUIC Require Import PCUICToTemplate.
 From Coq Require Import String.

diff --git a/extraction/theories/ConcordiumExtract.v b/extraction/theories/ConcordiumExtract.v
@@ -4,18 +4,18 @@ From Coq Require Import ZArith.
 
 From MetaCoq.Template Require Import All.
 From MetaCoq.Common Require Import Kernames.
-From ConCert.Utils Require Import StringExtra.
+From RustExtraction Require Import StringExtra.
 From ConCert.Execution Require Monad.
 From ConCert.Execution Require Import Blockchain.
-From ConCert.Extraction Require Import Common.
+From RustExtraction Require Import Common.
 From MetaCoq.Erasure.Typed Require Import Extraction.
 From MetaCoq.Erasure.Typed Require Import Optimize.
 From MetaCoq.Erasure.Typed Require Import ResultMonad.
 From MetaCoq.Erasure.Typed Require Import Utils.
-From ConCert.Extraction Require Import RustExtract.
+From RustExtraction Require Import RustExtract.
 From ConCert.Extraction Require Import SpecializeChainBase.
-From ConCert.Extraction Require Import PrettyPrinterMonad.
-From ConCert.Extraction Require Import Printing.
+From RustExtraction Require Import PrettyPrinterMonad.
+From RustExtraction Require Import Printing.
 
 Import MCMonadNotation.