diff options
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index d85a5f3f..30f5daf8 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -13,6 +13,9 @@ Tactics - Add Relation and Add Morphism on polymorphic relations should now be declared with Add Parametric Relation and Add Parametric Morphism. +- The constant [flip] is automatically unfolded in the goals generated by + Add Morphism (incompatibility with 8.2 beta versions). + - The default relation chosen by setoid_replace may differ. The workaround is to enforce the choice of the setoid relation with the "using relation ..." option. @@ -48,6 +51,9 @@ Tactics Language +- Type Class syntax has completely since the 8.2beta versions. See the + documentation for the updated syntax. + - Constants hidding polymorphic inductive types are now polymorphic themselves. This may exceptionally affect the naming of introduction hypotheses if such an inductive type in Type is used on |