From 38c47ac0626fed51d17bc7513d7dbbd63053016e Mon Sep 17 00:00:00 2001
From: Abhishek Anand (optiplex7010@home)
Date: Thu, 20 Feb 2020 19:52:39 -0800
Subject: added the new option

---
 interp/constrextern.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 38dc10a9b3..a5e7b89ded 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_parens = ref false
+
 (* This forces printing universe names of Type{.} *)
 let print_universes = Detyping.print_universes
 
-- 
cgit v1.2.3


From 5820b274acda8be0372471758842b0ea2b950d41 Mon Sep 17 00:00:00 2001
From: Abhishek Anand (optiplex7010@home)
Date: Sat, 22 Feb 2020 13:22:27 -0800
Subject: parens --> parentheses

---
 interp/constrextern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a5e7b89ded..bdfb63add3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -59,7 +59,7 @@ let print_coercions = ref false
 
 (* This forces printing of parentheses even when
    it is implied by associativity/precedence *)
-let print_parens = ref false
+let print_parentheses = ref false
 
 (* This forces printing universe names of Type{.} *)
 let print_universes = Detyping.print_universes
-- 
cgit v1.2.3


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/constrextern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bdfb63add3..3a0c6648cf 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -59,7 +59,7 @@ let print_coercions = ref false
 
 (* This forces printing of parentheses even when
    it is implied by associativity/precedence *)
-let print_parentheses = ref false
+let print_parentheses = Notation_ops.print_parentheses
 
 (* This forces printing universe names of Type{.} *)
 let print_universes = Detyping.print_universes
-- 
cgit v1.2.3