From f442efebd8354b233827e4991a80d27082c772e1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 24 Jul 2017 20:04:46 +0200 Subject: A little reorganization of notations + a fix to #5608. - Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation. --- interp/notation.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli index e63ad10cd..5f6bfa35f 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -21,7 +21,7 @@ open Ppextend (** A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters *) -type level = precedence * tolerability list +type level = precedence * tolerability list * notation_var_internalization_type list type delimiters = string type scope type scopes (** = [scope_name list] *) -- cgit v1.2.3