Move content of COMPATIBILITY to Changes chapter.

1 files changed, 200 insertions, 0 deletions

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 0620e09a4a..57b9e45342 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -843,6 +843,13 @@ system, is now upcoming and will rely on Inria’s newly created Foundation.
 | Matthieu Sozeau and the |Coq| development team
 |
 
+Potential compatibility issues
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+- Extra superfluous names in introduction patterns may now raise an
+  error rather than a warning when the superfluous name is already in
+  use. The easy fix is to remove the superfluous name.
+
 Details of changes in 8.7+beta1
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1232,6 +1239,30 @@ Dénès to put together a |Coq| consortium.
 | Matthieu Sozeau and the |Coq| development team
 |
 
+Potential sources of incompatibilities
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+- Symptom: An obligation generated by Program or an abstracted subproof
+  has different arguments.
+
+  Cause: Set Shrink Abstract and Set Shrink Obligations are on by default
+  and the subproof does not use the argument.
+
+  Remedy:
+
+  + Adapt the script.
+  + Write an explicit lemma to prove the obligation/subproof and use it
+    instead (compatible with 8.4).
+  + Unset the option for the program/proof the obligation/subproof originates
+    from.
+
+- Symptom: In a goal, order of hypotheses, or absence of an equality of
+  the form "x = t" or "t = x", or no unfolding of a local definition.
+
+  Cause: This might be connected to a number of fixes in the tactic
+  "subst". The former behavior can be reactivated by issuing "Unset
+  Regular Subst Tactic".
+
 Details of changes in 8.6beta1
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1580,6 +1611,124 @@ Tankink. Maxime Dénès coordinated the release process.
 | Hugo Herbelin, Matthieu Sozeau and the |Coq| development team
 |
 
+Potential sources of incompatibilities
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+List of typical changes to be done to adapt files from Coq 8.4
+to Coq 8.5 when not using compatibility option ``-compat 8.4``.
+
+- Symptom: "The reference omega was not found in the current environment".
+
+  Cause: "Require Omega" does not import the tactic "omega" any more
+
+  Possible solutions:
+
+  + use "Require Import OmegaTactic" (not compatible with 8.4)
+  + use "Require Import Omega" (compatible with 8.4)
+  + add definition "Ltac omega := Coq.omega.Omega.omega."
+
+- Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective)
+
+  Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives
+
+  Possible solutions:
+
+  + use "dintuition" instead; it is stronger than "intuition" and works
+    uniformly on non standard connectives, such as n-ary conjunctions or disjunctions
+    (not compatible with 8.4)
+  + do the script differently
+
+- Symptom: The constructor foo (in type bar) expects n arguments.
+
+  Cause: parameters must now be given in patterns
+
+  Possible solutions:
+
+  + use option "Set Asymmetric Patterns" (compatible with 8.4)
+  + add "_" for the parameters (not compatible with 8.4)
+  + turn the parameters into implicit arguments (compatible with 8.4)
+
+- Symptom: "NPeano.Nat.foo" not existing anymore\
+
+  Possible solutions:
+
+  + use "Nat.foo" instead
+
+  Symptom: typing problems with proj1_sig or similar
+
+  Cause: coercion from sig to sigT and similar coercions have been
+  removed so as to make the initial state easier to understand for
+  beginners
+
+  Solution: change proj1_sig into projT1 and similarly (compatible with 8.4)
+
+Other detailed changes
+
+- options for *coq* compilation (see below for ocaml).
+
+  + [-I foo] is now deprecated and will not add directory foo to the
+    coq load path (only for ocaml, see below). Just replace [-I foo] by
+    [-Q foo ""] in your project file and re-generate makefile. Or
+    perform the same operation directly in your makefile if you edit it
+    by hand.
+
+  + Option -R Foo bar is the same in v8.5 than in v8.4 concerning coq
+    load path.
+
+  + Option [-I foo -as bar] is unchanged but discouraged unless you
+    compile ocaml code. Use -Q foo bar instead.
+
+  for more details: see section "Customization at launch
+  time" of the reference manual.
+
+- Command line options for ocaml  Compilation of ocaml code (plugins)
+
+  + [-I foo] is *not* deprecated to add foo to the ocaml load path.
+
+  + [-I foo -as bar] adds foo to the ocaml load path *and* adds foo to
+    the coq load path with logical name bar (shortcut for -I foo -Q foo
+    bar).
+
+  for more details: section "Customization at launch
+  time" of the reference manual.
+
+- Universe Polymorphism.
+
+- Refinement, unification and tactics are now aware of universes,
+  resulting in more localized errors. Universe inconsistencies
+  should no more get raised at Qed time but during the proof.
+  Unification *always* produces well-typed substitutions, hence
+  some rare cases of unifications that succeeded while producing
+  ill-typed terms before will now fail.
+
+- The [change p with c] tactic semantics changed, now typechecking
+  [c] at each matching occurrence [t] of the pattern [p], and
+  converting [t] with [c].
+
+- Template polymorphic inductive types: the partial application
+  of a template polymorphic type (e.g. list) is not polymorphic.
+  An explicit parameter application (e.g [fun A => list A]) or
+  [apply (list _)] will result in a polymorphic instance.
+
+- The type inference algorithm now takes opacity of constants into
+  account. This may have effects on tactics using type inference
+  (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.
+
+Tactic abstract.
+
+- Auxiliary lemmas generated by the abstract tactic are removed from
+  the global environment and inlined in the proof term when a proof
+  is ended with Qed.  The behavior of 8.4 can be obtained by ending
+  proofs with "Qed exporting" or "Qed exporting ident, .., ident".
+
 Details of changes in 8.5beta1
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -2514,6 +2663,57 @@ Eelis van der Weegen.
 | Hugo Herbelin
 |
 
+Potential sources of incompatibilities
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The main known incompatibilities between 8.3 and 8.4 are consequences
+of the following changes:
+
+- The reorganization of the library of numbers:
+
+  Several definitions have new names or are defined in modules of
+  different names, but a special care has been taken to have this
+  renaming transparent for the user thanks to compatibility notations.
+
+  However some definitions have changed, what might require some
+  adaptations. The most noticeable examples are:
+
+  + The "?=" notation which now bind to Pos.compare rather than former
+    Pcompare (now Pos.compare_cont).
+  + Changes in names may induce different automatically generated
+    names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec").
+  + Z.add has a new definition, hence, applying "simpl" on subterms of
+    its body might give different results than before.
+  + BigN.shiftl and BigN.shiftr have reversed arguments order, the
+    power function in BigN now takes two BigN.
+
+- Other changes in libraries:
+
+  + The definition of functions over "vectors" (list of fixed length)
+    have changed.
+  + TheoryList.v has been removed.
+
+- Slight changes in tactics:
+
+  + Less unfolding of fixpoints when applying destruct or inversion on
+    a fixpoint hiding an inductive type (add an extra call to simpl to
+    preserve compatibility).
+  + Less unexpected local definitions when applying "destruct"
+    (incompatibilities solvable by adapting name hypotheses).
+  + Tactic "apply" might succeed more often, e.g. by now solving
+    pattern-matching of the form ?f x y = g(x,y) (compatibility
+    ensured by using "Unset Tactic Pattern Unification"), but also
+    because it supports (full) betaiota (using "simple apply" might
+    then help).
+  + Tactic autorewrite does no longer instantiate pre-existing
+    existential variables.
+  + Tactic "info" is now available only for auto, eauto and trivial.
+
+- Miscellaneous changes:
+
+  + The command "Load" is now atomic for backtracking (use "Unset
+    Atomic Load" for compatibility).
+
 Details of changes in 8.4beta
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~