From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- COMPATIBILITY | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'COMPATIBILITY') 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 -- cgit v1.2.3