Centralisation prod_name and co dans Environ; mkLambda_string dans Term

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

1 files changed, 7 insertions, 3 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index a83a8c6f23..3a58c92665 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -631,6 +631,10 @@ let abs_implicit c = mkLambda Anonymous mkImplicit c
 let lambda_implicit a = mkLambda (Name(id_of_string"y")) mkImplicit a
 let lambda_implicit_lift n a = iterate lambda_implicit n (lift n a)
 
+let mkLambda_string s t c = mkLambda (Name (id_of_string s)) t c
+let mkProd_string   s t c = mkProd (Name (id_of_string s)) t c
+
+
 (* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *)
 let prod_it = List.fold_left (fun c (n,t)  -> mkProd n t c)
 
@@ -1177,9 +1181,9 @@ let sort_increasing_snd =
 	 (_,Rel m),(_,Rel n) -> m < n
        | _ -> assert false)
 
-(* Recognizing occurrences of a given subterm in a term for Pattern :
-   (subst_term c t) substitutes (Rel 1) for all occurrences of term c 
-   in a (closed) term t *)
+(* Recognizing occurrences of a given (closed) subterm in a term for Pattern :
+   [subst_term c t] substitutes [(Rel 1)] for all occurrences of (closed)
+   term [c] in a term [t] *)
 
 let subst_term c t = 
   let rec substrec k c t =