From a872ab42a338e0e9ccb5d1586b10fb961b66d425 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 22 Jan 2018 10:37:46 +0100 Subject: Move the mention of the removal of Qed exporting at the right place. --- CHANGES | 3 +++ COMPATIBILITY | 4 ---- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/CHANGES b/CHANGES index c9197fb36e..cb5da333aa 100644 --- a/CHANGES +++ b/CHANGES @@ -51,6 +51,9 @@ Focusing Vernacular Commands +- Proofs ending in "Qed exporting ident, .., ident" are not supported + anymore. Constants generated during `abstract` are kept private to the + local environment. - The deprecated Coercion Local, Open Local Scope, Notation Local syntax was removed. Use Local as a prefix instead. - For the Extraction Language command, "OCaml" is spelled correctly. diff --git a/COMPATIBILITY b/COMPATIBILITY index b5fed7f018..78dfabaa3e 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -5,10 +5,6 @@ Potential sources of incompatibilities between Coq V8.6 and V8.7 error rather than a warning when the superfluous name is already in use. The easy fix is to remove the superfluous name. -- Proofs ending in "Qed exporting ident, .., ident" are not supported - anymore. Constants generated during `abstract` are kept private to the - local environment. - Potential sources of incompatibilities between Coq V8.5 and V8.6 ---------------------------------------------------------------- -- cgit v1.2.3 From e8c32132796582b792f0b9a154fe568446526e95 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 22 Jan 2018 10:40:51 +0100 Subject: Archive COMPATIBILITY. --- COMPATIBILITY | 198 ------------------------------------------------- dev/doc/COMPATIBILITY | 201 ++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 201 insertions(+), 198 deletions(-) delete mode 100644 COMPATIBILITY create mode 100644 dev/doc/COMPATIBILITY diff --git a/COMPATIBILITY b/COMPATIBILITY deleted file mode 100644 index 78dfabaa3e..0000000000 --- a/COMPATIBILITY +++ /dev/null @@ -1,198 +0,0 @@ -Potential sources of incompatibilities between Coq V8.6 and V8.7 ----------------------------------------------------------------- - -- 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. - -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". diff --git a/dev/doc/COMPATIBILITY b/dev/doc/COMPATIBILITY new file mode 100644 index 0000000000..a81afca32d --- /dev/null +++ b/dev/doc/COMPATIBILITY @@ -0,0 +1,201 @@ +Note: this file isn't used anymore. Incompatibilities are documented +as part of CHANGES. + +Potential sources of incompatibilities between Coq V8.6 and V8.7 +---------------------------------------------------------------- + +- 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. + +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". -- cgit v1.2.3