diff options
| author | ppedrot | 2012-09-14 16:17:09 +0000 |
|---|---|---|
| committer | ppedrot | 2012-09-14 16:17:09 +0000 |
| commit | f8394a52346bf1e6f98e7161e75fb65bd0631391 (patch) | |
| tree | ae133cc5207283e8c5a89bb860435b37cbf6ecdb /kernel/indtypes.ml | |
| parent | 6dae53d279afe2b8dcfc43dd2aded9431944c5c8 (diff) | |
Moving Utils.list_* to a proper CList module, which includes stdlib
List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 6c7f4408f7..b93b9f19b1 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -351,7 +351,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = let compute_rec_par (env,n,_,_) hyps nmr largs = if nmr = 0 then 0 else (* start from 0, hyps will be in reverse order *) - let (lpar,_) = list_chop nmr largs in + let (lpar,_) = List.chop nmr largs in let rec find k index = function ([],_) -> nmr @@ -375,7 +375,7 @@ let abstract_mind_lc env ntyps npars lc = lc else let make_abs = - list_tabulate + List.tabulate (function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps in Array.map (substl make_abs) lc @@ -457,7 +457,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname let auxnpar = mib.mind_nparams_rec in let nonrecpar = mib.mind_nparams - auxnpar in let (lpar,auxlargs) = - try list_chop auxnpar largs + try List.chop auxnpar largs with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in (* If the inductive appears in the args (non params) then the definition is not positive. *) @@ -539,7 +539,7 @@ let check_positivity kn env_ar params inds = let nmr = rel_context_nhyps params in let check_one i (_,lcnames,lc,(sign,_)) = let ra_env = - list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in + List.tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in let nargs = rel_context_nhyps sign - nmr in check_positivity_one ienv params (kn,i) nargs lcnames lc |