From ca3a49011901e09d5e3488d8c9ffb165e420f192 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Wed, 8 Apr 2020 10:48:14 -0400
Subject: [PATCH] Revising before class

---
 DeepAndShallowEmbeddings.v | 2 +-
 DeepInterp.ml              | 2 ++
 DeeperInterp.ml            | 2 ++
 DeeperWithFailInterp.ml    | 2 ++
 4 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v
index 29e89ea..e81ca1b 100644
--- a/DeepAndShallowEmbeddings.v
+++ b/DeepAndShallowEmbeddings.v
@@ -332,7 +332,7 @@ Module Deep.
   | Write (a v : nat) : cmd unit.
 
   (* These constructors are most easily explained through examples.  We'll
-   * translate both of the programs from the shallowly embedding above. *)
+   * translate both of the programs from the shallow embedding above. *)
 
   Notation "x <- c1 ; c2" := (Bind c1 (fun x => c2)) (right associativity, at level 80).
 
diff --git a/DeepInterp.ml b/DeepInterp.ml
index e98482f..0abe128 100644
--- a/DeepInterp.ml
+++ b/DeepInterp.ml
@@ -1,3 +1,5 @@
+open Deep
+
 let rec i2n n =
   match n with
   | 0 -> O
diff --git a/DeeperInterp.ml b/DeeperInterp.ml
index 1edf9b8..c95bc03 100644
--- a/DeeperInterp.ml
+++ b/DeeperInterp.ml
@@ -1,3 +1,5 @@
+open Deeper
+
 let rec i2n n =
   match n with
   | 0 -> O
diff --git a/DeeperWithFailInterp.ml b/DeeperWithFailInterp.ml
index f44a5b8..b878db6 100644
--- a/DeeperWithFailInterp.ml
+++ b/DeeperWithFailInterp.ml
@@ -1,3 +1,5 @@
+open DeeperWithFail
+
 let rec i2n n =
   match n with
   | 0 -> O