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.mli | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'printing/ppconstr.mli')

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