v0.11.2

Added

• Bind notation allowing for type cast annotations of variables (#93)
• let* monadic notation (#95, by #96)

Changed

• Functor_Fun and Applicative_Fun instances are global (#88, by #90)

Fixed

• Data: bug fix in TwoThreeK (#86)

v0.11.1

Fixed

• Notation ;; back to right associative
• Notation >>= binds tighter than ;;

v0.11.0

Added

• Core: decideP function yielding {P} + {~P} for Decidable propositions. (#81)
• Programming: curry function in Extras module.
• Structures:
  • MonadLaws are back. (#31, by #80)
  • Functor instance for Applicative. (#77)
• Tactics:
  • Rewrite hypotheses;
  • Clear trivial hypotheses;
  • Hide and show hypotheses. (#81)

Changed

• Data: make vector template-polymorphic again. (#76)

Removed

• Module:
  • Core: Type;
  • Structures: Identity and Proper;
  • Tactics: TypeTac;
• Class: PFunctor, PApplicative, and PMonad. (#80)

Fixed

• Operator precedence difference from Haskell. (#78, by #80)

v0.10.3

Added

• CoMonadLaws class. (#63)

Changed

• CoMonad functions: renamed coret to extract, and cobind to extend. (#63)
  coret and extract are still available as aliases, for backward compatibility.

Fixed

• Monad and notations conflict. (#66, by #68)

v0.10.2

With some additional facts about finite maps.

v0.10.1

Release compatible with Coq 8.9 and includes some extra definitions around hlists.

v0.10.0

A few new features and bug fixes.

v0.9.8 (Coq 8.8)

Coq 8.8 support

v0.9.7 (coq.8.7)

Coq 8.7 compatibility.

v0.9.5 (coq.8.6)

Bug fix release for compatibility with Coq 8.6.