diff options
Diffstat (limited to 'plugins/syntax')
| -rw-r--r-- | plugins/syntax/g_numeral.mlg (renamed from plugins/syntax/g_numeral.ml4) | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.mlg index 55f61a58f9..5dbc9eea7a 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.mlg @@ -10,6 +10,8 @@ DECLARE PLUGIN "numeral_notation_plugin" +{ + open Notation open Numeral open Pp @@ -24,15 +26,17 @@ let pr_numnot_option _ _ _ = function | Warning n -> str "(warning after " ++ str n ++ str ")" | Abstract n -> str "(abstract after " ++ str n ++ str ")" +} + ARGUMENT EXTEND numnotoption - PRINTED BY pr_numnot_option -| [ ] -> [ Nop ] -| [ "(" "warning" "after" bigint(waft) ")" ] -> [ Warning waft ] -| [ "(" "abstract" "after" bigint(n) ")" ] -> [ Abstract n ] + PRINTED BY { pr_numnot_option } +| [ ] -> { Nop } +| [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft } +| [ "(" "abstract" "after" bigint(n) ")" ] -> { Abstract n } END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> - [ vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o ] + { vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o } END |