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).
---
 interp/constrexpr.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'interp/constrexpr.ml')

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 1d51109b7f..4bdacda529 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -20,8 +20,12 @@ type ident_decl = lident * universe_decl_expr option
 type name_decl = lname * universe_decl_expr option
 
 type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
+
+type entry_level = int
+type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | LevelSome
+
 type notation_entry = InConstrEntry | InCustomEntry of string
-type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int
+type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * entry_level
 type notation_key = string
 
 (* A notation associated to a given parsing rule *)
-- 
cgit v1.2.3