diff options
| author | Pierre-Marie Pédrot | 2018-10-12 09:22:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-15 22:55:55 +0200 |
| commit | 4da233a9685cd193a84def037ec18a27c9225dce (patch) | |
| tree | e4ba7de73cc815d9f4ead92a83dc18c28883d316 /plugins/syntax | |
| parent | 8e7131b65894e9e549422cb47aab5a3a357a6352 (diff) | |
Port remaining EXTEND ml4 files to coqpp.
Almost all of ml4 were removed in the process. The only remaining files
are in the test-suite and probably need a bit of fiddling with coq_makefile,
and there only two really remaning ml4 files containing code.
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 |