Spracherkennung für: .mlg vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
DECLARE PLUGIN "rocq-runtime.plugins.evil"
{
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
[Dauer der Verarbeitung: 0.17 Sekunden, vorverarbeitet 2026-06-04]
