diff options
| -rw-r--r-- | COMPATIBILITY | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index 1595445293..1ed4b25d0a 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -22,6 +22,24 @@ Tactics - Add Relation and Add Morphism on polymorphic relations should now be declared with Add Parametric Relation and Add Parametric Morphism. +- 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. + +- The ordering of subgoals generated by setoid_rewrite and + setoid_replace tactics has been changed. Some reordering in the + proof script may be necessary. You may also use the 'by ...' option + of setoid_replace and setoid_rewrite. + +- The definition of Setoid_Theory has changed. When using the + constructors of the structure, you need to unfold the definitions + Reflexive, Symmetric, and Transitive. + +- The names of bound variables of theorems generated by Add Morphism + differs, which may cause some problems with scripts that do not name + variable when perform introductions. Changing intros to the + appropriate intro x x0 ... xn should fix the problem. + - Some bug fixes may lead to incompatibilities (see CHANGES for a detailed account). |