From 61f2f55a08dcef612c538ec7e6d0864d86fe3e0a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 23 Feb 2020 17:09:21 +0100
Subject: Not iterating recursive notations more than once.

---
 interp/notation_ops.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d1eb50d370..9f052278ad 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
-- 
cgit v1.2.3