diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 8cc69f4d1b..3480d1c8f2 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -219,6 +219,7 @@ type notation_rule_core = type notation_rule = notation_rule_core * delimiters option (* delimiter to possibly add *) + * bool (* true if the delimiter is mandatory *) (** Return the possible notations for a given term *) val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list |