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).
---
 plugins/ltac/pptactic.mli | 29 ++++++++++++++---------------
 1 file changed, 14 insertions(+), 15 deletions(-)

(limited to 'plugins/ltac/pptactic.mli')

diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 9cff3ea1eb..33db933168 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -16,7 +16,6 @@ open Geninterp
 open Names
 open Environ
 open Constrexpr
-open Notation_gram
 open Genintern
 open Tacexpr
 open Tactypes
@@ -29,43 +28,43 @@ type 'a raw_extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) ->
   'a -> Pp.t
 
 type 'a glob_extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) ->
   'a -> Pp.t
 
 type 'a extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
   'a -> Pp.t
 
 type 'a raw_extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
-  tolerability -> 'a -> Pp.t
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) ->
+  entry_relative_level -> 'a -> Pp.t
 
 type 'a glob_extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
-  tolerability -> 'a -> Pp.t
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) ->
+  entry_relative_level -> 'a -> Pp.t
 
 type 'a extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
-  tolerability -> 'a -> Pp.t
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+  entry_relative_level -> 'a -> Pp.t
 
 val declare_extra_genarg_pprule :
   ('a, 'b, 'c) genarg_type ->
@@ -78,7 +77,7 @@ val declare_extra_genarg_pprule_with_level :
   'a raw_extra_genarg_printer_with_level ->
   'b glob_extra_genarg_printer_with_level ->
   'c extra_genarg_printer_with_level ->
-  (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit
+  (* surroounded *) entry_relative_level -> (* non-surroounded *) entry_relative_level -> unit
 
 val declare_extra_vernac_genarg_pprule :
   ('a, 'b, 'c) genarg_type ->
@@ -140,7 +139,7 @@ val pr_ltac_constant : ltac_constant -> Pp.t
 
 val pr_raw_tactic : env -> Evd.evar_map -> raw_tactic_expr -> Pp.t
 
-val pr_raw_tactic_level : env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t
+val pr_raw_tactic_level : env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t
 
 val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t
 
@@ -155,10 +154,10 @@ val pr_match_pattern : ('a -> Pp.t) -> 'a match_pattern -> Pp.t
 val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) ->
   ('b, 'a) match_rule -> Pp.t
 
-val pr_value : tolerability -> Val.t -> Pp.t
+val pr_value : entry_relative_level -> Val.t -> Pp.t
 
 
-val ltop : tolerability
+val ltop : entry_relative_level
 
-val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) ->
+val make_constr_printer : (env -> Evd.evar_map -> entry_relative_level -> 'a -> Pp.t) ->
   'a Genprint.top_printer
-- 
cgit v1.2.3