diff options
| author | Pierre-Marie Pédrot | 2018-10-19 16:21:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-19 16:24:46 +0200 |
| commit | 266050f7aaa0ee0b090b30b1acabaccda6919889 (patch) | |
| tree | 290d511d83edbdd9709ccd2ec32c0ec05904c6ce /test-suite/misc | |
| parent | 3f6eebb9cfeda531d1f71e2ea0fa2d5afa9c28fc (diff) | |
Porting the test-suite to coqpp.
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 |