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 ++++
 interp/constrextern.mli | 1 +
 2 files changed, 5 insertions(+)

(limited to 'interp')

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
 
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index fa263cbeb7..2691d27f69 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_parens : bool ref
 val print_universes : bool ref
 val print_no_symbol : bool ref
 val print_projections : bool ref
-- 
cgit v1.2.3