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