diff options
| author | Emilio Jesus Gallego Arias | 2020-02-22 13:51:55 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-22 13:51:55 -0500 |
| commit | fd67afe0f7c55799ae0a14d78f1007a0360bd552 (patch) | |
| tree | 7b77866dfda1c468eb3a0ddddd1afcd22af1a834 /parsing/ppextend.mli | |
| parent | 7ef010c50c9d8efcd20d44807126efcd418c4e0d (diff) | |
| parent | 2e64c61cf64172fb0dce2d8b3996fb30e179e5ea (diff) | |
Merge PR #11635: Cleanup around the tolerability structure
Reviewed-by: ejgallego
Diffstat (limited to 'parsing/ppextend.mli')
| -rw-r--r-- | parsing/ppextend.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli index 7996e7696d..346fc83f5f 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 - | 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 -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 |