diff options
| author | Enrico Tassi | 2014-09-24 17:37:10 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-29 21:54:31 +0200 |
| commit | 8f118b444db7693dcc16dda4c271d2528bfa949a (patch) | |
| tree | a01df0fd808a3d17b1e3d12d7710225c533bfe12 /intf | |
| parent | ec49447d078da25959d617ae23e55a668fdd1646 (diff) | |
Notation: option to attach extra pretty printing rules to notations
so that one can retrieve them and pass them to third party tools (i.e.
print the AST with the notations attached to the nodes concerned).
Available syntax:
- all in one:
Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2").
- a posteriori:
Format Notation "a /\ b" "latex" "#1 \wedge #2".
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index e670f68c21..2c73a974b5 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -206,7 +206,7 @@ type syntax_modifier = | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing of Flags.compat_version - | SetFormat of string located + | SetFormat of string * string located type proof_end = | Admitted @@ -290,6 +290,7 @@ type vernac_expr = | VernacNotation of obsolete_locality * constr_expr * (lstring * syntax_modifier list) * scope_name option + | VernacNotationAddFormat of string * string * string (* Gallina *) | VernacDefinition of |