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 /printing/prettyp.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 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 86b2da2eb0..7fbbc0a2ec 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -93,7 +93,7 @@ let print_impargs_by_name max = function let print_one_impargs_list l = let imps = List.filter is_status_implicit l in let maximps = List.filter Impargs.maximal_insertion_of imps in - let nonmaximps = list_subtract imps maximps in + let nonmaximps = List.subtract imps maximps in print_impargs_by_name false nonmaximps @ print_impargs_by_name true maximps @@ -127,7 +127,7 @@ let need_expansion impl ref = let ctx = (prod_assum typ) in let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in impl <> [] & List.length impl >= nprods & - let _,lastimpl = list_chop nprods impl in + let _,lastimpl = List.chop nprods impl in List.filter is_status_implicit lastimpl <> [] let print_impargs ref = |