Revert "A heuristic to add parentheses in the presence of rules such as"

This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.

6 files changed, 15 insertions, 41 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 1a2e7074f..b8f4f3201 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -965,7 +965,7 @@ let pr_visibility prglob = function
 (**********************************************************************)
 (* Mapping notations to concrete syntax *)
 
-type unparsing_rule = unparsing list * precedence * tolerability option
+type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
 (* Concrete syntax for symbolic-extension table *)
 let printing_rules =
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
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 7fad6fb9a..1866ca504 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -85,8 +85,8 @@ end) = struct
         mt ()
       | UnpMetaVar (_, prec) as unp :: l ->
         let c = pop env in
-        let pp1= pr (n, prec) c in
         let pp2 = aux l in
+        let pp1 = pr (n, prec) c in
         return unp pp1 pp2
       | UnpListMetaVar (_, prec, sl) as unp :: l ->
         let cl = pop envlist in
@@ -95,16 +95,15 @@ end) = struct
         return unp pp1 pp2
       | UnpBinderListMetaVar (_, isopen, sl) as unp :: l ->
         let cl = pop bll in
-        let pp1 = pr_binders (fun () -> aux sl) isopen cl in
         let pp2 = aux l in
+        let pp1 = pr_binders (fun () -> aux sl) isopen cl in
         return unp pp1 pp2
       | UnpTerminal s as unp :: l ->
-        let pp1 = str s in
         let pp2 = aux l in
+        let pp1 = str s in
         return unp pp1 pp2
       | UnpBox (b,sub) as unp :: l ->
-        let pp1 = aux sub in
-        let pp1 = ppcmd_of_box b pp1 in
+        let pp1 = ppcmd_of_box b (aux sub) in
         let pp2 = aux l in
         return unp pp1 pp2
       | UnpCut cut as unp :: l ->
@@ -115,12 +114,8 @@ end) = struct
     aux unps
 
   let pr_notation pr pr_binders s env =
-    let unpl, level, trailing_level = find_notation_printing_rule s in
-    let pp = print_hunks level pr pr_binders env unpl in
-    let level = match trailing_level with
-      | Some (level',_) -> max level level'
-      | _ -> level in
-    pp, level 
+    let unpl, level = find_notation_printing_rule s in
+    print_hunks level pr pr_binders env unpl, level
 
   let pr_delimiters key strm =
     strm ++ str ("%"^key)
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 593a5df84..6ff1d3837 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -54,7 +54,3 @@ end
      : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
 exist (Q x) y conj
      : {x0 : A | Q x x0}
-fun x : nat => (## x) + x
-     : nat -> nat
-fun x : nat => ## x + x
-     : nat -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index d32758375..4e0d135d7 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -106,10 +106,3 @@ Check fun x (H:le x 0) => exist (le x) 0 H.
 
 Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
 Check (exist (Q x) y conj).
-
-(* Check printing of notations that have arguments at higher level
-   than the notation itself *)
-
-Notation "## a" := (S a) (at level 0, a at level 100).
-Check fun x => (S x) + x.
-Check fun x => S (x + x).
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e0cdc1b62..7c1f05cd3 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -479,14 +479,6 @@ let make_hunks etyps symbols from =
 
   in make symbols
 
-let rec trailing_precedence etyps from = function
-  | [] -> assert false
-  | [NonTerminal id|SProdList (id,_)] ->
-     let typ = List.assoc id etyps in
-     Some (precedence_of_entry_type from typ)
-  | [Terminal _|Break _] -> None
-  | _ :: l -> trailing_precedence etyps from l
-
 (* Build default printing rules from explicit format *)
 
 let error_format () = error "The format does not match the notation."
@@ -680,7 +672,7 @@ type syntax_extension = {
   synext_level : Notation.level;
   synext_notation : notation;
   synext_notgram : notation_grammar;
-  synext_unparsing : unparsing_rule;
+  synext_unparsing : unparsing list;
   synext_extra : (string * string) list;
 }
 
@@ -699,7 +691,7 @@ let cache_one_syntax_extension se =
     Egramcoq.extend_constr_grammar prec se.synext_notgram;
     (* Declare the printing rule *)
     Notation.declare_notation_printing_rule ntn
-      ~extra:se.synext_extra se.synext_unparsing
+      ~extra:se.synext_extra (se.synext_unparsing, fst prec)
 
 let cache_syntax_extension (_, (_, sy)) =
   List.iter cache_one_syntax_extension sy
@@ -1059,7 +1051,7 @@ exception NoSyntaxRule
 let recover_syntax ntn =
   try
     let prec = Notation.level_of_notation ntn in
-    let pp_rule= Notation.find_notation_printing_rule ntn in
+    let pp_rule,_ = Notation.find_notation_printing_rule ntn in
     let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in
     let pa_rule = Egramcoq.recover_constr_grammar ntn prec in
     { synext_level = prec;
@@ -1093,16 +1085,14 @@ let make_pa_rule i_typs (n,typs,symbols,_) ntn =
     notgram_prods = prod;
     notgram_typs = i_typs; }
 
-let make_pp_rule (n,typs,symbols,fmt) (lev,_) =
-  let unp = match fmt with
+let make_pp_rule (n,typs,symbols,fmt) =
+  match fmt with
   | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
-  | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) in
-  let trailingprec = trailing_precedence typs lev symbols in
-  (unp, lev, trailingprec)
+  | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt)
 
 let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra =
   let pa_rule = make_pa_rule i_typs sy_data ntn in
-  let pp_rule = make_pp_rule sy_data prec in
+  let pp_rule = make_pp_rule sy_data in
   let sy = {
     synext_level = prec;
     synext_notation = ntn;