Potential sources of incompatibilities between Coq V8.5 and V8.6 ---------------------------------------------------------------- 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". Potential sources of incompatibilities between Coq V8.4 and V8.5 ---------------------------------------------------------------- * 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 * (see also file 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: file CHANGES or 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: file CHANGES or 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". 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".