diff options
Diffstat (limited to 'grammar/vernacextend.ml4')
| -rw-r--r-- | grammar/vernacextend.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 029755f08..3074337f6 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")) |