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 /grammar | |
| 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 'grammar')
| -rw-r--r-- | grammar/grammar.mllib | 1 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 6 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 2 |
3 files changed, 5 insertions, 4 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 006766e17c..6849669dbd 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -8,6 +8,7 @@ Loc Segmenttree Unicodetable Errors +CList Util Bigint Hashcons diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 87425ef54a..f38479ac90 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -53,7 +53,7 @@ let rec extract_signature = function let check_unicity s l = let l' = List.map (fun (l,_) -> extract_signature l) l in - if not (Util.list_distinct l') then + if not (Util.List.distinct l') then Pp.msg_warning (strbrk ("Two distinct rules of tactic entry "^s^" have the same "^ "non-terminals in the same order: put them in distinct tactic entries")) @@ -152,10 +152,10 @@ let rec possibly_empty_subentries loc = function else possibly_empty_subentries loc l let possibly_atomic loc prods = - let l = list_map_filter (function + let l = List.map_filter (function | GramTerminal s :: l, _ -> Some (s,l) | _ -> None) prods in - possibly_empty_subentries loc (list_factorize_left l) + possibly_empty_subentries loc (List.factorize_left l) let declare_tactic loc s cl = let se = mlexpr_of_string s in diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 029755f081..3074337f66 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -30,7 +30,7 @@ let rec make_let e = function let check_unicity s l = let l' = List.map (fun (_,l,_) -> extract_signature l) l in - if not (Util.list_distinct l') then + if not (Util.List.distinct l') then Pp.msg_warning (strbrk ("Two distinct rules of entry "^s^" have the same "^ "non-terminals in the same order: put them in distinct vernac entries")) |