diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /COMPATIBILITY | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'COMPATIBILITY')
-rw-r--r-- | COMPATIBILITY | 191 |
1 files changed, 0 insertions, 191 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY deleted file mode 100644 index d423e71d..00000000 --- a/COMPATIBILITY +++ /dev/null @@ -1,191 +0,0 @@ -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". |