*** empty log message ***

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

2 files changed, 28 insertions, 6 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index f9a1bed147..736734365e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -996,6 +996,9 @@ let prodn n env b =
   in 
   prodrec (n,env,b)
 
+(* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
+let compose_prod l b = prodn (List.length l) l b
+
 (* lamn n [xn:Tn;..;x1:T1;Gamma] b = [x1:T1]..[xn:Tn]b *)
 let lamn n env b =
   let rec lamrec = function
@@ -1005,6 +1008,9 @@ let lamn n env b =
   in 
   lamrec (n,env,b)
 
+(* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *)
+let compose_lam l b = lamn (List.length l) l b
+
 let applist (f,l) = mkApp (f, Array.of_list l)
 
 let applistc f l = mkApp (f, Array.of_list l)
@@ -1013,8 +1019,8 @@ let appvect = mkApp
 	    
 let appvectc f l = mkApp (f,l)
 		     
-(* to_lambda n (x1:T1)...(xn:Tn)(xn+1:Tn+1)...(xn+j:Tn+j)T =
- * [x1:T1]...[xn:Tn](xn+1:Tn+1)...(xn+j:Tn+j)T *)
+(* to_lambda n (x1:T1)...(xn:Tn)T =
+ * [x1:T1]...[xn:Tn]T *)
 let rec to_lambda n prod =
   if n = 0 then 
     prod 
diff --git a/kernel/term.mli b/kernel/term.mli
index 1e7a6e08e0..472ffb2c87 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -80,7 +80,7 @@ val body_of_type : types -> constr
 
 (*s Term constructors. *)
 
-(* Constructs a DeBrujin index *)
+(* Constructs a DeBrujin index (DB indices begin at 1) *)
 val mkRel : int -> constr
 
 (* Constructs a Variable *)
@@ -325,7 +325,6 @@ val mkNamedProd_wo_LetIn : named_declaration -> types -> types
 val mkLambda_or_LetIn : rel_declaration -> constr -> constr
 val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr
 
-
 (*s Other term constructors. *)
 
 val abs_implicit : constr -> constr
@@ -343,14 +342,28 @@ val appvectc : constr -> constr array -> constr
    where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *)
 val prodn : int -> (name * constr) list -> constr -> constr
 
+(* [compose_prod l b] = $(x_1:T_1)..(x_n:T_n)b$
+   where $l = [(x_n,T_n);\dots;(x_1,T_1)]$.
+   Inverse of [decompose_prod]. *)
+val compose_prod : (name * constr) list -> constr -> constr
+
 (* [lamn n l b] = $[x_1:T_1]..[x_n:T_n]b$
    where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *)
 val lamn : int -> (name * constr) list -> constr -> constr
 
+(* [compose_lam l b] = $[x_1:T_1]..[x_n:T_n]b$
+   where $l = [(x_n,T_n);\dots;(x_1,T_1)]$.
+   Inverse of [decompose_lam] *)
+val compose_lam : (name * constr) list -> constr -> constr
+
 (* [to_lambda n l] 
-   = $[x_1:T_1]...[x_n:T_n](x_{n+1}:T_{n+1})...(x_{n+j}:T_{n+j})T$
-   where $l = (x_1:T_1)...(x_n:T_n)(x_{n+1}:T_{n+1})...(x_{n+j}:T_{n+j})T$ *)
+   = $[x_1:T_1]...[x_n:T_n]T$
+   where $l = (x_1:T_1)...(x_n:T_n)T$ *)
 val to_lambda : int -> constr -> constr
+
+(* [to_prod n l] 
+   = $(x_1:T_1)...(x_n:T_n)T$
+   where $l = [x_1:T_1]...[x_n:T_n]T$ *)
 val to_prod : int -> constr -> constr
 
 (* pseudo-reduction rule *)
@@ -415,6 +428,9 @@ val noccur_with_meta : int -> int -> constr -> bool
 
 (*s Relocation and substitution *)
 
+(* [exliftn el c] lifts [c] with lifting [el] *)
+val exliftn : Esubst.lift -> constr -> constr
+
 (* [liftn n k c] lifts by [n] indexes above [k] in [c] *)
 val liftn : int -> int -> constr -> constr