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.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'interp/notation_ops.mli')

diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index c62dac013b..d235f87580 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 *
-- 
cgit v1.2.3