diff options
| author | courant | 2003-06-27 13:35:03 +0000 |
|---|---|---|
| committer | courant | 2003-06-27 13:35:03 +0000 |
| commit | afe6690652949d92bfbcf34194836364884b7111 (patch) | |
| tree | 5a5dc1f4c8c681f6cb2156dd6083a4671364e700 /kernel/term.ml | |
| parent | 293b31aab50f0b7f947960ce15bf9ae6b6d576de (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4209 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 10 |
1 files changed, 8 insertions, 2 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 |