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/ppextend.mli | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'parsing/ppextend.mli')

diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 7996e7696d..8ea6f31241 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Constrexpr
-open Notation_gram
 
 (** {6 Pretty-print. } *)
 
@@ -31,15 +30,15 @@ val ppcmd_of_cut : ppcut -> Pp.t
 
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing =
-  | UnpMetaVar of int * parenRelation
-  | UnpBinderMetaVar of int * parenRelation
-  | UnpListMetaVar of int * parenRelation * unparsing list
+  | UnpMetaVar of int * entry_relative_level
+  | UnpBinderMetaVar of int * entry_relative_level
+  | UnpListMetaVar of int * entry_relative_level * unparsing list
   | UnpBinderListMetaVar of int * bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
   | UnpCut of ppcut
 
-type unparsing_rule = unparsing list * precedence
+type unparsing_rule = unparsing list * entry_level
 type extra_unparsing_rules = (string * string) list
 
 val unparsing_eq : unparsing -> unparsing -> bool
-- 
cgit v1.2.3


From 1d840bf16744717e3289afaf66db4c44a7f7d814 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Feb 2020 01:34:35 +0100
Subject: Simplification of type unparsing (index of variable in UnpMetaVar is
 unused).

---
 parsing/ppextend.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'parsing/ppextend.mli')

diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 8ea6f31241..346fc83f5f 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -30,10 +30,10 @@ val ppcmd_of_cut : ppcut -> Pp.t
 
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing =
-  | UnpMetaVar of int * entry_relative_level
-  | UnpBinderMetaVar of int * entry_relative_level
-  | UnpListMetaVar of int * entry_relative_level * unparsing list
-  | UnpBinderListMetaVar of int * bool * unparsing list
+  | UnpMetaVar of entry_relative_level
+  | UnpBinderMetaVar of entry_relative_level
+  | UnpListMetaVar of entry_relative_level * unparsing list
+  | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
   | UnpCut of ppcut
-- 
cgit v1.2.3