fact: Definition change A {B} (f : ttac A) : ttac B := (oeq <- M.unify A B UniCoq; match oeq with | mSome eq => match eq in Logic.meq _ X return ttac X with | Logic.meq_refl => f end | mNone => M.raise TTchange_Exception end )%MC.
imports: Mtac2(Base Datatypes List Sorts tactics.Tactics) Strings.String