blob: bb6eaff409582c2eb14bbb58d1ed55b2667094ea (
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 Constrexpr in
DeclareUniv.do_constraint ~poly:false [ CType (Libnames.qualid_of_ident i), Univ.Lt, CType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT()
}
END
|
