Changes from v1.1.1 to v1.2 =========================== - Now project hosted in GitHub. - Fixpoint notation supports up to 5 arguments. - Restriction in abs to ensure soundness (see paper). - Other minor bug fixes. Changes from v1.1 to v1.1.1 =========================== - Fixed bug preventing Ssreflect to compile. Changes from v1.0 to v1.1 ========================= - New name for the monad: Mtac instead of T. But there is a notation M for it. - New notation for fixpoint: mfix f (x : A) (y : B) (z : C) : M D := body It supports up to three arguments, and all the typing annotations are optional. - Return accepts three forms for shaping the returned term: * ret t : it just returns the term t. * retS t : it simplifies t before returning it. This was the default in v1.0. * retW t : it performs whd reduction to t before returning it. - The level of the @@ and >> notation for bind changed from 90 to 70 to avoid conflict with the Containers library. - The unification algorithm is patched to solve eagerly some simple equations, in order to make Mtac run faster. - Bug fixed: the unification variables are not removed after unifying the pattern in the mmatch. This was causing some troubles, and it is not changing the semantics of Mtac. - Bug fixed: Unification variables are not required to be instantiated after unification of the pattern. This is useful in cases when the pattern unification variable is instantiated with another unification variable.