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 /plugins/decl_mode/decl_interp.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 'plugins/decl_mode/decl_interp.ml')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 5e128bc423..f2f978ccdf 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -57,7 +57,7 @@ let intern_hyp iconstr globs = function Hprop (intern_statement iconstr globs st) let intern_hyps iconstr globs hyps = - snd (list_fold_map (intern_hyp iconstr) globs hyps) + snd (List.fold_map (intern_hyp iconstr) globs hyps) let intern_cut intern_it globs cut= let nglobs,nstat=intern_it globs cut.cut_stat in @@ -74,10 +74,10 @@ let intern_hyp_list args globs = let intern_one globs (loc,(id,opttyp)) = (add_var id globs), (loc,(id,Option.map (intern_constr globs) opttyp)) in - list_fold_map intern_one globs args + List.fold_map intern_one globs args let intern_suffices_clause globs (hyps,c) = - let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in + let nglobs,nhyps = List.fold_map (intern_hyp intern_constr) globs hyps in nglobs,(nhyps,intern_constr_or_thesis nglobs c) let intern_fundecl args body globs= @@ -340,7 +340,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (fun (loc,(id,_)) -> GVar (loc,id)) params in let dum_args= - list_tabulate + List.tabulate (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false))) oib.Declarations.mind_nrealargs in glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in |