diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index f3ecbd446f..424cb93ef7 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -288,7 +288,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function let declare_notation_level ntn level = if Gmap.mem ntn !notation_level_map then - error ("Notation "^ntn^" is already assigned a level"); + anomaly ("Notation "^ntn^" is already assigned a level"); notation_level_map := Gmap.add ntn level !notation_level_map let level_of_notation ntn = |