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/genprint.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'printing/genprint.ml')

diff --git a/printing/genprint.ml b/printing/genprint.ml
index a04df31d30..a673cbd933 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -19,15 +19,15 @@ open Geninterp
 (* Printing generic values *)
 
 type 'a with_level =
-  { default_already_surrounded : Notation_gram.tolerability;
-    default_ensure_surrounded : Notation_gram.tolerability;
+  { default_already_surrounded : Constrexpr.entry_relative_level;
+    default_ensure_surrounded : Constrexpr.entry_relative_level;
     printer : 'a }
 
 type printer_result =
 | PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t)
-| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level
+| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t) with_level
 
-type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t
 
 type top_printer_result =
 | TopPrinterBasic of (unit -> Pp.t)
-- 
cgit v1.2.3