diff options
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")) |