From 8b2c4ea19c7930939c6d6d540558f042a60ac391 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Dec 2019 23:37:41 +0100
Subject: Making structure of type "tolerability" and related clearer.

Also renamed it to relative_entry_level.

Correspondence between old and new representation is:
(n,L) -> LevelLt n
(n,E), (n,Prec n) -> LevelLe n
(n,Any) -> LevelSome
(n,Prec p) when n<>p was unused

Should not change global semantics (except error message in pr_arg).
---
 printing/ppconstr.mli | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'printing/ppconstr.mli')

diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index c17ca251a8..288fb251c4 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -15,9 +15,8 @@
 open Libnames
 open Constrexpr
 open Names
-open Notation_gram
 
-val prec_less : precedence -> tolerability -> bool
+val prec_less : entry_level -> entry_relative_level -> bool
 
 val pr_tight_coma : unit -> Pp.t
 
@@ -49,7 +48,7 @@ val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr
 val pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t
 val pr_lconstr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t
 val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t
-val pr_constr_expr_n : Environ.env -> Evd.evar_map -> tolerability -> constr_expr -> Pp.t
+val pr_constr_expr_n : Environ.env -> Evd.evar_map -> entry_relative_level -> constr_expr -> Pp.t
 
 type term_pr = {
   pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t;
@@ -76,8 +75,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. *)
 
-val lsimpleconstr : tolerability
-val ltop : tolerability
+val lsimpleconstr : entry_relative_level
+val ltop : entry_relative_level
 val modular_constr_pr :
-  ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) ->
-  (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t
+  ((unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t) ->
+  (unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t
-- 
cgit v1.2.3