diff options
| author | Hugo Herbelin | 2018-09-24 23:14:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | 9bc339f529fc2ee2389a717914514829a73686bc (patch) | |
| tree | 5ccbfe4c7e6cb1c6c5648830a5f1debda4e19926 /interp/notation.mli | |
| parent | 06fc6caa49b67526cf3521d1b5885aae6710358b (diff) | |
Fixing #8551 (missing delimiters when notation exists both lonely and in scope).
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 |