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

This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.

1 files changed, 6 insertions, 11 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 7fad6fb9ab..1866ca5042 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)