COMPATIBILITY

Potential sources of incompatibilities between Coq V8.4 and V8.5
----------------------------------------------------------------

(see also file CHANGES)

* 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 *

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".

Potential sources of incompatibilities between Coq V8.3 and V8.4
----------------------------------------------------------------

(see also file CHANGES)

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).


Incompatibilities beyond 8.4...

- Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is
  now "A -> (B <-> C)"

- Tactics: tauto and intuition no longer accidentally destruct binary
  connectives or records other than and, or, prod, sum, iff. In most
  of cases, dtauto or dintuition, though stronger than 8.3 tauto and
  8.3 intuition will provide compatibility.

- "Solve Obligations using" is now "Solve Obligations with".