Merge PR #11650: Set Printing Parens

Reviewed-by: ejgallego

4 files changed, 10 insertions, 0 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4ec9f17c71..44aacd62d8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -57,6 +57,10 @@ let print_implicits_defensive = ref true
 (* This forces printing of coercions *)
 let print_coercions = ref false
 
+(* This forces printing of parentheses even when
+   it is implied by associativity/precedence *)
+let print_parentheses = Notation_ops.print_parentheses
+
 (* This forces printing universe names of Type{.} *)
 let print_universes = Detyping.print_universes
 
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index fa263cbeb7..0eca287c1d 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -53,6 +53,7 @@ val print_implicits_defensive : bool ref
 val print_arguments : bool ref
 val print_evar_arguments : bool ref
 val print_coercions : bool ref
+val print_parentheses : bool ref
 val print_universes : bool ref
 val print_no_symbol : bool ref
 val print_projections : bool ref
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 59a58d643c..8f47e9276b 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -258,6 +258,8 @@ let glob_constr_of_notation_constr ?loc x =
 (******************************************************************************)
 (* Translating a glob_constr into a notation, interpreting recursive patterns *)
 
+let print_parentheses = ref false
+
 type found_variables = {
     vars : Id.t list;
     recursive_term_vars : (Id.t * Id.t) list;
@@ -1092,6 +1094,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin revert =
       let rest = Id.List.assoc ldots_var terms in
       let t = Id.List.assoc y terms in
       let sigma = remove_sigma y (remove_sigma ldots_var sigma) in
+      if !print_parentheses && not (List.is_empty acc) then raise No_match;
       aux sigma (t::acc) rest
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 2ab8b620df..0ef51b65a2 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -61,6 +61,8 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const
 
 exception No_match
 
+val print_parentheses : bool ref
+
 val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
       ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list *
       ('a cases_pattern_disjunction_g * extended_subscopes) list *