From c616bd4d9819e4cd3c868716cb92663b3c69e069 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 31 Oct 2017 15:38:40 +0100
Subject: Removing a redundancy in naming types (Ppconstr.precedence =
 tolerability).

---
 printing/ppconstr.ml  | 1 -
 printing/ppconstr.mli | 9 ++++-----
 2 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 102c6ef6de..4d7a716319 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -738,7 +738,6 @@ let tag_var = tag Tag.variable
     pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
   }
 
-  type precedence =  Notation_term.precedence * Notation_term.parenRelation
   let modular_constr_pr = pr
   let rec fix rf x = rf (fix rf) x
   let pr = fix modular_constr_pr mt
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 7546c748d8..34cccfc2d0 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -86,9 +86,8 @@ val default_term_pr : term_pr
   Which has the same type. We can turn a modular printer into a printer by
   taking its fixpoint. *)
 
-type precedence
-val lsimpleconstr : precedence
-val ltop : precedence
+val lsimpleconstr : tolerability
+val ltop : tolerability
 val modular_constr_pr :
-  ((unit->Pp.t) -> precedence -> constr_expr -> Pp.t) ->
-  (unit->Pp.t) -> precedence  -> constr_expr -> Pp.t
+  ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) ->
+  (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t
-- 
cgit v1.2.3