diff options
| author | Hugo Herbelin | 2019-12-25 23:37:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 01:52:29 +0100 |
| commit | 8b2c4ea19c7930939c6d6d540558f042a60ac391 (patch) | |
| tree | 1892276e77bc54938fc53aa1e1a3056a5006ff79 /parsing/ppextend.mli | |
| parent | b5bd769d725495d8c78c04d6721742e602a9b539 (diff) | |
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).
Diffstat (limited to 'parsing/ppextend.mli')
| -rw-r--r-- | parsing/ppextend.mli | 9 |
1 files changed, 4 insertions, 5 deletions
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 |