← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to COMPATIBILITY

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
COMPATIBILITY
 
1
Potential sources of incompatibilities between Coq V8.1 and V8.2
 
2
----------------------------------------------------------------
 
3
 
 
4
(see also file CHANGES)
 
5
 
 
6
Tactics
 
7
 
 
8
- The apply tactic now unfolds the constants if needed to succeed.  As
 
9
  a consequence, use of "try apply" or "repeat apply" or "apply" in
 
10
  other Ltac potentially backtracking code may behave differently. Use
 
11
  "simple apply" instead.
 
12
 
 
13
- Add Relation and Add Morphism on polymorphic relations should now be
 
14
  declared with Add Parametric Relation and Add Parametric Morphism.
 
15
 
 
16
- The constant [flip] is automatically unfolded in the goals generated by
 
17
  Add Morphism (incompatibility with 8.2 beta versions).
 
18
 
 
19
- The default relation chosen by setoid_replace may differ. The
 
20
  workaround is to enforce the choice of the setoid relation with the
 
21
  "using relation ..." option.
 
22
 
 
23
- The ordering of subgoals generated by setoid_rewrite and
 
24
  setoid_replace tactics has been changed. Some reordering in the
 
25
  proof script may be necessary. You may also use the 'by ...' option
 
26
  of setoid_replace and setoid_rewrite.
 
27
  
 
28
- The definition of Setoid_Theory has changed. When using the
 
29
  constructors of the structure, you need to unfold the definitions
 
30
  Reflexive, Symmetric, and Transitive.
 
31
 
 
32
- The names of bound variables of theorems generated by Add Morphism
 
33
  differs, which may cause some problems with scripts that do not name
 
34
  variable when perform introductions. Changing intros to the
 
35
  appropriate intro x x0 ... xn should fix the problem.
 
36
 
 
37
- Tactic firstorder "with" and "using" options have their meaning
 
38
  swapped for consistency with auto/eauto. The solution is to swap
 
39
  the use of these options in call to firstorder.
 
40
 
 
41
- Introduction patterns are more strict. In "intros [ ... | ... | ... ] H",
 
42
  the names in the brackets are synchronized so that H denotes the same
 
43
  hypothesis in every subgoal.
 
44
 
 
45
- Application patterns with a meta variable in function position (?X ?Y) now
 
46
  match arbitrary applications as expected. Use a nested 
 
47
  [match X with (_ _) => fail 1 | _ => ..] to recover the old semantics.
 
48
 
 
49
- Some bug fixes may lead to incompatibilities (see CHANGES for a detailed
 
50
  account).
 
51
 
 
52
Language
 
53
 
 
54
- Type Class syntax has completely since the 8.2beta versions. See the
 
55
  documentation for the updated syntax.
 
56
 
 
57
- Constants hidding polymorphic inductive types are now polymorphic
 
58
  themselves. This may exceptionally affect the naming of
 
59
  introduction hypotheses if such an inductive type in Type is used on
 
60
  small types such as Prop or Set: the hypothesis names suffix will
 
61
  default to H instead of X.
 
62
 
 
63
Libraries
 
64
 
 
65
- Some changes in the library (as mentioned in the CHANGES file) may
 
66
  imply the need for local adaptations. This may particularly be the
 
67
  case with the move from Set to Type in libraries FSets, SetoidList,
 
68
  ListSet, Sorting and Zmisc. In case of trouble it may help to simply
 
69
  declare Set as an alias for Type (see file SetIsType).
 
70
 
 
71
For the main changes in the ML interfaces, see file
 
72
dev/doc/changes.txt in the main archive.