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.