aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cbv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cbv.ml')
-rw-r--r--pretyping/cbv.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2599e2958..58d461e57 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -27,12 +27,12 @@ open Esubst
* in normal form and neutral (i.e. not a lambda, a construct or a
* (co)fix, because they may produce redexes by applying them,
* or putting them in a case)
- * LAM(x,a,b,S) is the term [S]([x:a]b). the substitution is propagated
+ * LAM(x,a,b,S) is the term [S]([x:a]b). the bindings is propagated
* only when the abstraction is applied, and then we use the rule
* ([S]([x:a]b) c) --> [S.c]b
* This corresponds to the usual strategy of weak reduction
* FIXP(op,bd,S,args) is the fixpoint (Fix or Cofix) of bodies bd under
- * the substitution S, and then applied to args. Here again,
+ * the bindings S, and then applied to args. Here again,
* weak reduction.
* CONSTR(c,args) is the constructor [c] applied to [args].
*
@@ -67,8 +67,8 @@ let rec shift_value n = function
CONSTR (c, List.map (shift_value n) args)
-(* Contracts a fixpoint: given a fixpoint and a substitution,
- * returns the corresponding fixpoint body, and the substitution in which
+(* Contracts a fixpoint: given a fixpoint and a bindings,
+ * returns the corresponding fixpoint body, and the bindings in which
* it should be evaluated: its first variables are the fixpoint bodies
* (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1}))
* -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti)
@@ -204,7 +204,7 @@ let rec norm_head info env t stack =
| LetIn (x, b, t, c) ->
(* zeta means letin are contracted; delta without zeta means we *)
- (* allow substitution but leave let's in place *)
+ (* allow bindings but leave let's in place *)
let zeta = red_set (info_flags info) fZETA in
let env' =
if zeta