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


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7

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