Ajout {prod,lambda}_name

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

2 files changed, 20 insertions, 3 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index b58145fc30..77f470b8bf 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -194,10 +194,12 @@ let named_hd env a = function
   | x         -> x
 
 let prod_name env (n,a,b) = mkProd (named_hd env a n) a b
+let lambda_name env (n,a,b) = mkLambda (named_hd env a n) a b
 
-let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous) a b
+let it_prod_name env = List.fold_left (fun c (n,t) ->prod_name env (n,t,c)) 
+let it_lambda_name env = List.fold_left (fun c (n,t) ->lambda_name env (n,t,c))
 
-let lambda_name env (n,a,b) = mkLambda (named_hd env a n) a b
+let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous) a b
 
 (* Abstractions. *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f9b17b76de..1d3dcd4c14 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -51,10 +51,25 @@ val lookup_mind_specif : inductive -> env -> mind_specif
 val id_of_global : env -> sorts oper -> identifier
 
 val id_of_name_using_hdchar : env -> constr -> name -> identifier
+
+(* [named_hd env t na] just returns [na] is it defined, otherwise it
+   creates a name built from [t] (e.g. ["n"] if [t] is [nat]) *)
+
 val named_hd : env -> constr -> name -> name
+
+(* The following functions build product or abstraction and create
+   names using [named_hd] for unnamed binders *)
+
+val lambda_name : env -> name * constr * constr -> constr
 val prod_name : env -> name * constr * constr -> constr
+val it_lambda_name : env -> constr -> (name * constr) list -> constr
+val it_prod_name : env -> constr -> (name * constr) list -> constr
+
+(* [lambda_create env (t,c)] builds [[x:t]c] where [x] is a name built
+   from [t] *)
+
 val lambda_create : env -> constr * constr -> constr
-val lambda_name : env -> name * constr * constr -> constr
+
 
 val translucent_abst : env -> constr -> bool
 val evaluable_abst : env -> constr -> bool