diff options
Diffstat (limited to 'pretyping/indrec.ml')
| -rw-r--r-- | pretyping/indrec.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 025f7f668..f11fb4613 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -134,7 +134,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let d = (n,Some b,t) in mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c) | Ind (_,_) -> - let realargs = list_skipn nparams largs in + let realargs = List.skipn nparams largs in let base = applist (lift i pk,realargs) in if depK then Reduction.beta_appvect @@ -209,7 +209,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let d = (n,Some b,t) in mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c) | Ind _ -> - let realargs = list_skipn nparrec largs + let realargs = List.skipn nparrec largs and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in applist(lift i fk,realargs@[arg]) | _ -> assert false @@ -431,7 +431,7 @@ let mis_make_indrec env sigma listdepkind mib = mis_make_case_com dep env sigma indi (mibi,mipi) kind in (* Body of mis_make_indrec *) - list_tabulate make_one_rec nrec + List.tabulate make_one_rec nrec (**********************************************************************) (* This builds elimination predicate for Case tactic *) |