fact: Definition tc_unify_mtac T (A B : T) := o <- @M.unify T A B UniCoq; match o with | mSome eq => M.ret eq | mNone => let A := reduce (RedStrong RedAll) A in let B := reduce (RedStrong RedAll) B in M.failwith "cannot (tc_)unify." end.
imports: Coq.Strings.String Mtac2(Base Specif Logic Datatypes MTele MTeleMatchDef)