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