diff options
Diffstat (limited to 'test-suite/misc')
| -rw-r--r-- | test-suite/misc/poly-capture-global-univs/_CoqProject | 2 | ||||
| -rw-r--r-- | test-suite/misc/poly-capture-global-univs/src/evil.ml4 | 9 | ||||
| -rw-r--r-- | test-suite/misc/poly-capture-global-univs/src/evil.mlg | 10 |
3 files changed, 11 insertions, 10 deletions
diff --git a/test-suite/misc/poly-capture-global-univs/_CoqProject b/test-suite/misc/poly-capture-global-univs/_CoqProject index 70ec246062..e5dc3cff56 100644 --- a/test-suite/misc/poly-capture-global-univs/_CoqProject +++ b/test-suite/misc/poly-capture-global-univs/_CoqProject @@ -1,7 +1,7 @@ -Q theories Evil -I src -src/evil.ml4 +src/evil.mlg src/evilImpl.ml src/evilImpl.mli src/evil_plugin.mlpack diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 b/test-suite/misc/poly-capture-global-univs/src/evil.ml4 deleted file mode 100644 index 565e979aaa..0000000000 --- a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 +++ /dev/null @@ -1,9 +0,0 @@ - -open Stdarg -open EvilImpl - -DECLARE PLUGIN "evil_plugin" - -VERNAC COMMAND FUNCTIONAL EXTEND VernacEvil CLASSIFIED AS SIDEFF -| [ "Evil" ident(x) ident(y) ] -> [ fun ~atts ~st -> evil x y; st ] -END diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.mlg b/test-suite/misc/poly-capture-global-univs/src/evil.mlg new file mode 100644 index 0000000000..edd22b1d29 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evil.mlg @@ -0,0 +1,10 @@ +{ +open Stdarg +open EvilImpl +} + +DECLARE PLUGIN "evil_plugin" + +VERNAC COMMAND EXTEND VernacEvil CLASSIFIED AS SIDEFF +| [ "Evil" ident(x) ident(y) ] -> { evil x y } +END |