diff options
| author | Enrico Tassi | 2018-10-29 11:21:54 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-10-29 11:21:54 +0100 |
| commit | 60b7d3662880666a22e0b90f55b49361c453e3f4 (patch) | |
| tree | 3eb42248e0ef9a251dbedb4f28b88288682c6bba /test-suite/misc | |
| parent | 8d6e79649a3f7696977954de881671c23457c0f2 (diff) | |
| parent | 266050f7aaa0ee0b090b30b1acabaccda6919889 (diff) | |
Merge PR #8763: Adapt coq_makefile to handle coqpp-based macro files.
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 |