Merge PR #11650: Set Printing Parens

Reviewed-by: ejgallego

1 files changed, 3 insertions, 0 deletions

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