diff options
| author | herbelin | 1999-12-11 01:25:22 +0000 |
|---|---|---|
| committer | herbelin | 1999-12-11 01:25:22 +0000 |
| commit | 20445e418ffee0c0dc1398c80af4a2b75abe9ac3 (patch) | |
| tree | c019077ca3898406ef9f251b26dba4ec06d24d2d /kernel/term.ml | |
| parent | d73ae1a52442841ec8c067de7048db977b299a85 (diff) | |
Intégration initiale du Cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@234 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 31e52ebb3f..f2e8d34227 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -592,7 +592,7 @@ let lambda_implicit_lift n a = iterate lambda_implicit n (lift n a) (* prod_it b [x1:T1;..xn:Tn] = (x1:T1)..(xn:Tn)b *) let prod_it = List.fold_left (fun c (n,t) -> mkProd n t c) -(* lam_it b [x1:T1;..xn:Tn] = [x1:T1]..[xn:Tn]b *) +(* lam_it b [x1:T1;..xn:Tn] = [x1:T1]..[xn:Tn]b with xn *) let lam_it = List.fold_left (fun c (n,t) -> mkLambda n t c) (* prodn n ([x1:T1]..[xn:Tn]Gamma) b = (x1:T1)..(xn:Tn)b *) @@ -665,19 +665,19 @@ let rec to_prod n lam = * if this does not work, then we use the string S as part of our * error message. *) -let prod_app s t n = +let prod_app t n = match strip_outer_cast t with | DOP2(Prod,_,b) -> sAPP b n | _ -> - errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ; - 'sTR s ; 'fNL >] + errorlabstrm "prod_app" + [< 'sTR"Needed a product, but didn't find one" ; 'fNL >] -(* prod_appvect s T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_appvect s t nL = Array.fold_left (prod_app s) t nL +(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) +let prod_appvect t nL = Array.fold_left prod_app t nL -(* prod_applist s T [ a1 ; ... ; an ] -> (T a1 ... an) *) -let prod_applist s t nL = List.fold_left (prod_app s) t nL +(* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) +let prod_applist t nL = List.fold_left prod_app t nL (*********************************) |