diff options
| author | Hugo Herbelin | 2020-07-14 15:57:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-15 17:38:36 +0100 |
| commit | 3ac39cdd88368c62aa25eaa37fb61fb16406e180 (patch) | |
| tree | 42bac084dab407796ed30816a2b70a6909f1eaf1 /interp/notation.mli | |
| parent | 534d44074d0c4464b425ba9d7d92be8dda04d5ac (diff) | |
Moving the analysis of notation strings in notation.ml.
This is a better abstraction barrier (no "symbol" type with
uninterpreted ".." exported out of notation.ml). It also allows to
"browse" notations mentioning a "..".
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index b8939ff87b..97955bf92e 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -334,8 +334,10 @@ val symbol_eq : symbol -> symbol -> bool val make_notation_key : notation_entry -> symbol list -> notation val decompose_notation_key : notation -> notation_entry * symbol list -(** Decompose a notation of the form "a 'U' b" *) -val decompose_raw_notation : string -> symbol list +(** Decompose a notation of the form "a 'U' b" together with the lists + of pairs of recursive variables and the list of all variables + binding in the notation *) +val decompose_raw_notation : string -> (Id.t * Id.t) list * Id.t list * symbol list (** Prints scopes (expects a pure aconstr printer) *) val pr_scope_class : scope_class -> Pp.t |