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/ssr/ssrparser.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ssr/ssrparser.mli')

diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index e6b1706b41..53c895f9d9 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -15,12 +15,12 @@ open Ltac_plugin
 val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
 val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
 val pr_ssrtacarg : Environ.env -> Evd.evar_map -> 'a -> 'b ->
-  (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c) -> 'c
+  (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c) -> 'c
 
 val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
 val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
 val pr_ssrtclarg : Environ.env -> Evd.evar_map -> 'a -> 'b ->
-  (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
+  (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c -> 'd) -> 'c -> 'd
 
 val add_genarg : string -> (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> 'a Genarg.uniform_genarg_type
 
-- 
cgit v1.2.3