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

2 files changed, 13 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 =
diff --git a/kernel/term.mli b/kernel/term.mli
index 51406b1e08..7320b8be89 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -164,6 +164,9 @@ val mkCast : constr -> constr -> constr
 (* Constructs the product $(x:t_1)t_2$. $x$ may be anonymous. *)
 val mkProd : name -> constr -> constr -> constr
 
+(* [mkProd_string s t c] constructs the product $(s:t)c$ *)
+val mkProd_string : string -> constr -> constr -> constr
+
 (* non-dependant product $t_1 \rightarrow t_2$ *)
 val mkArrow : constr -> constr -> constr
 
@@ -174,6 +177,9 @@ val mkNamedProd : identifier -> constr -> constr -> constr
 val mkLambda : name -> constr -> constr -> constr
 val mkNamedLambda : identifier -> constr -> constr -> constr
 
+(* [mkLambda_string s t c] constructs $[s:t]c$ *)
+val mkLambda_string : string -> constr -> constr -> constr
+
 (* If $a = [| t_1; \dots; t_n |]$, constructs the application 
    $(t_1~\dots~t_n)$. *)
 val mkAppL : constr array -> constr