From 1abd56dea147493178a582569f50c9c6f03c6008 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 19 May 2003 17:35:03 +0000 Subject: Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/cbv.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'pretyping/cbv.ml') 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 -- cgit v1.2.3