Cancelling precedences in Set Printing Parentheses only at border of notations.

4 files changed, 24 insertions, 24 deletions

diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index 393ab8a302..bb6693a239 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -38,9 +38,9 @@ let ppcmd_of_cut = function
   | PpBrk(n1,n2) -> brk(n1,n2)
 
 type unparsing =
-  | UnpMetaVar of entry_relative_level
+  | UnpMetaVar of entry_relative_level * Extend.side option
   | UnpBinderMetaVar of entry_relative_level
-  | UnpListMetaVar of entry_relative_level * unparsing list
+  | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option
   | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
@@ -50,9 +50,9 @@ type unparsing_rule = unparsing list * entry_level
 type extra_unparsing_rules = (string * string) list
 
 let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
-  | UnpMetaVar p1, UnpMetaVar p2 -> entry_relative_level_eq p1 p2
+  | UnpMetaVar (p1,s1), UnpMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2
   | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2
-  | UnpListMetaVar (p1,l1), UnpListMetaVar (p2,l2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2
+  | UnpListMetaVar (p1,l1,s1), UnpListMetaVar (p2,l2,s2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 && s1 = s2
   | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2
   | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2
   | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2)
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 346fc83f5f..18e48942c6 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -30,9 +30,9 @@ val ppcmd_of_cut : ppcut -> Pp.t
 
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing =
-  | UnpMetaVar of entry_relative_level
+  | UnpMetaVar of entry_relative_level * Extend.side option
   | UnpBinderMetaVar of entry_relative_level
-  | UnpListMetaVar of entry_relative_level * unparsing list
+  | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option
   | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d96a528b76..59972f8bdb 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -93,19 +93,19 @@ let tag_var = tag Tag.variable
     let rec aux = function
       | [] ->
         mt ()
-      | UnpMetaVar prec as unp :: l ->
+      | UnpMetaVar (prec, side) as unp :: l ->
         let c = pop env in
         let pp2 = aux l in
-        let pp1 = pr (if parens then LevelLe 0 else prec) c in
+        let pp1 = pr (if parens && side <> None then LevelLe 0 else prec) c in
         return unp pp1 pp2
       | UnpBinderMetaVar prec as unp :: l ->
         let c = pop bl in
         let pp2 = aux l in
         let pp1 = pr_patt prec c in
         return unp pp1 pp2
-      | UnpListMetaVar (prec, sl) as unp :: l ->
+      | UnpListMetaVar (prec, sl, side) as unp :: l ->
         let cl = pop envlist in
-        let pp1 = prlist_with_sep (fun () -> aux sl) (pr (if parens then LevelLe 0 else prec)) cl in
+        let pp1 = prlist_with_sep (fun () -> aux sl) (pr (if parens && side <> None then LevelLe 0 else prec)) cl in
         let pp2 = aux l in
         return unp pp1 pp2
       | UnpBinderListMetaVar (isopen, sl) as unp :: l ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index afff0347f5..3937f887ad 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -294,15 +294,15 @@ let precedence_of_position_and_level from_level = function
      | RightA, Right -> LevelLe n
      | LeftA, Left -> LevelLe n
      | LeftA, Right -> LevelLt n
-     | NonA, _ -> LevelLt n)
-  | NumLevel n, _ -> LevelLe n
-  | NextLevel, _ -> LevelLt from_level
-  | DefaultLevel, _ -> LevelSome
+     | NonA, _ -> LevelLt n), Some b
+  | NumLevel n, _ -> LevelLe n, None
+  | NextLevel, _ -> LevelLt from_level, None
+  | DefaultLevel, _ -> LevelSome, None
 
 (** Computing precedences of subentries for parsing *)
 let precedence_of_entry_type (from_custom,from_level) = function
   | ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
-    precedence_of_position_and_level from_level x
+    fst (precedence_of_position_and_level from_level x)
   | ETConstr (custom,_,(NumLevel n,_)) -> LevelLe n
   | ETConstr (custom,_,(NextLevel,_)) ->
     user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++
@@ -323,9 +323,9 @@ let unparsing_precedence_of_entry_type from_level = function
     (* Precedence of printing for a custom entry is managed using
        explicit insertion of entry coercions at the time of building
        a [constr_expr] *)
-    LevelSome
-  | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0)
-  | _ -> LevelSome (* should not matter *)
+    LevelSome, None
+  | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0), None
+  | _ -> LevelSome, None (* should not matter *)
 
 (* Some breaking examples *)
 (* "x = y" : "x /1 = y" (breaks before any symbol) *)
@@ -392,10 +392,10 @@ let check_open_binder isopen sl m =
 
 let unparsing_metavar i from typs =
   let x = List.nth typs (i-1) in
-  let prec = unparsing_precedence_of_entry_type from x in
+  let prec,side = unparsing_precedence_of_entry_type from x in
   match x with
   | ETConstr _ | ETGlobal | ETBigint ->
-     UnpMetaVar prec
+     UnpMetaVar (prec,side)
   | ETPattern _ ->
      UnpBinderMetaVar prec
   | ETIdent ->
@@ -446,14 +446,14 @@ let make_hunks etyps symbols from_level =
     | SProdList (m,sl) :: prods ->
         let i = index_id m vars in
         let typ = List.nth typs (i-1) in
-        let prec = unparsing_precedence_of_entry_type from_level typ in
+        let prec,side = unparsing_precedence_of_entry_type from_level typ in
         let sl' =
           (* If no separator: add a break *)
           if List.is_empty sl then add_break 1 []
           (* We add NonTerminal for simulation but remove it afterwards *)
           else make true sl in
         let hunk = match typ with
-          | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl')
+          | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl',side)
           | ETBinder isopen ->
               check_open_binder isopen sl m;
               UnpBinderListMetaVar (isopen,List.map snd sl')
@@ -589,13 +589,13 @@ let hunks_of_format (from_level,(vars,typs)) symfmt =
   | SProdList (m,sl) :: symbs, fmt when has_ldots fmt ->
       let i = index_id m vars in
       let typ = List.nth typs (i-1) in
-      let prec = unparsing_precedence_of_entry_type from_level typ in
+      let prec,side = unparsing_precedence_of_entry_type from_level typ in
       let loc_slfmt,rfmt = read_recursive_format sl fmt in
       let sl, slfmt = aux (sl,loc_slfmt) in
       if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) ();
       let symbs, l = aux (symbs,rfmt) in
       let hunk = match typ with
-        | ETConstr _ -> UnpListMetaVar (prec,slfmt)
+        | ETConstr _ -> UnpListMetaVar (prec,slfmt,side)
         | ETBinder isopen ->
             check_open_binder isopen sl m;
             UnpBinderListMetaVar (isopen,slfmt)