untyped eval: tweaks

diff --git a/code/untyped_evaluator.ml b/code/untyped_evaluator.ml
index edfc6ee..50092fb 100644 (file)
--- a/code/untyped_evaluator.ml
+++ b/code/untyped_evaluator.ml
@@ -72,7 +72,7 @@ let rec lookup (sought_ident : ident) (env : env) : term option =
    eval raises this exception when it fails to reduce/evaluate
    a term, because it has components for which no
    reduction/evaluation is defined, such as `x y`. The
    eval raises this exception when it fails to reduce/evaluate
    a term, because it has components for which no
    reduction/evaluation is defined, such as `x y`. The

-   reduction-based interpreter just signals this with a normal
+   substitute-and-repeat interpreter just signals this with a normal

    return value; but the environment-based interpreter uses an
    exception to abort prematurely.
 
    return value; but the environment-based interpreter uses an
    exception to abort prematurely.
 

diff --git a/code/untyped_evaluator_complete.ml b/code/untyped_evaluator_complete.ml
index 930491f..51efce9 100644 (file)
--- a/code/untyped_evaluator_complete.ml
+++ b/code/untyped_evaluator_complete.ml
@@ -72,7 +72,7 @@ let rec lookup (sought_ident : ident) (env : env) : term option =
    eval raises this exception when it fails to reduce/evaluate
    a term, because it has components for which no
    reduction/evaluation is defined, such as `x y`. The
    eval raises this exception when it fails to reduce/evaluate
    a term, because it has components for which no
    reduction/evaluation is defined, such as `x y`. The

-   reduction-based interpreter just signals this with a normal
+   substitute-and-repeat interpreter just signals this with a normal

    return value; but the environment-based interpreter uses an
    exception to abort prematurely.
 
    return value; but the environment-based interpreter uses an
    exception to abort prematurely.