From c5b6321df0f83d6b29489bbddb920bdb1ebb96a8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 27 Apr 2016 22:13:04 +0200 Subject: Revert "A heuristic to add parentheses in the presence of rules such as" This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15. --- 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 352c20313..480979ccc 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -194,7 +194,7 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd (** {6 Printing rules for notations} *) (** Declare and look for the printing rule for symbolic notations *) -type unparsing_rule = unparsing list * precedence * tolerability option +type unparsing_rule = unparsing list * precedence type extra_unparsing_rules = (string * string) list val declare_notation_printing_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit -- cgit v1.2.3