diff options
Diffstat (limited to 'test-suite/misc/side-eff-leak-univs/src/evil.mlg')
| -rw-r--r-- | test-suite/misc/side-eff-leak-univs/src/evil.mlg | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg new file mode 100644 index 0000000000..d89ab887a8 --- /dev/null +++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg @@ -0,0 +1,13 @@ +DECLARE PLUGIN "evil_plugin" + +{ +open Ltac_plugin +open Stdarg +} + +TACTIC EXTEND magic +| [ "magic" ident(i) ident(j) ] -> { + let open Glob_term in + DeclareUniv.do_constraint ~poly:false [ GType (Libnames.qualid_of_ident i), Univ.Lt, GType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT() +} +END |