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).
---
 parsing/notation_gram.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'parsing/notation_gram.ml')

diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 9f133ca9d4..2fa9a496b7 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -10,14 +10,11 @@
 
 open Names
 open Extend
+open Constrexpr
 
 (** Dealing with precedences *)
 
-type precedence = int
-type parenRelation = L | E | Any | Prec of precedence
-type tolerability = precedence * parenRelation
-
-type level = Constrexpr.notation_entry * precedence * tolerability list * constr_entry_key list
+type level = notation_entry * entry_level * entry_relative_level list * constr_entry_key list
   (* first argument is InCustomEntry s for custom entries *)
 
 type grammar_constr_prod_item =
-- 
cgit v1.2.3