Only import WASM-TEXT in DRIVER, not in EWASM

kframework · Jun 13, 2020 · de5f4da · de5f4da
1 parent e3609a0
commit de5f4da
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/driver.md b/driver.md
@@ -2,16 +2,19 @@ Ethereum Simulation
 ===================
 
 ```k
+require "wasm-text.md"
 require "ewasm.md"
 require "data.md"
 
 module DRIVER-SYNTAX
     imports EWASM-SYNTAX
+    imports WASM-TEXT-SYNTAX
     imports DRIVER
 endmodule
 
 module DRIVER
     imports EWASM
+    imports WASM-TEXT
 ```
 
 An Ewasm program is the invocation of an Ethereum contract containing Ewasm code.

diff --git a/ewasm.md b/ewasm.md
@@ -2,11 +2,11 @@ Ewasm Specification
 =================
 
 ```k
-require "wasm-text.md"
+require "wasm.md"
 require "eei.md"
 
 module EWASM-SYNTAX
-    imports WASM-TEXT-SYNTAX
+    imports WASM-SYNTAX
     imports EWASM
 endmodule
 ```
@@ -19,7 +19,7 @@ Ewasm consists of a WebAssembly (Wasm) semantics, and an Ethereum Environment In
 
 ```k
     imports EEI
-    imports WASM-TEXT
+    imports WASM
 ```
 
 The configuration composes both the top level cells of the Wasm and EEI semantics.