blob: d89ab887a8f2de6b1ef67bf6d92fdc2a2b41e875 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
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
|
