diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-02-12 22:59:41 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-02-12 22:59:41 +0100 |
| commit | 1e1a2f1803c57cc1697e294a7610b76a95661687 (patch) | |
| tree | cc683aa3b940c36ab3f5c692693bfeeb257855d4 /COMPATIBILITY | |
| parent | 8c5bfa0f00b80979473bba26c1b9a1410667e032 (diff) | |
COMPATIBILITY: add note about the change of behavior of Instance foo :=
{| |}. Add test-suite files for closed bugs.
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index 2ce29346c..3b4e8987c 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -26,6 +26,13 @@ Universe Polymorphism. (e.g. induction). Extra "Transparent" might have to be added to revert opacity of constants. +Type classes. + +- When writing an Instance foo : Class A := {| proj := t |} (note the + vertical bars), support for typechecking the projections using the + type information and switching to proof mode is no longer available. + Use { } (without the vertical bars) instead. + Potential sources of incompatibilities between Coq V8.3 and V8.4 ---------------------------------------------------------------- |