diff options
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 48 |
1 files changed, 45 insertions, 3 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index 55b2d003f7..892eaa599e 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -1,7 +1,19 @@ -Potential sources of incompatibilities between Coq V8.4 and V8.5 +Potential sources of incompatibilities between Coq V8.5 and V8.6 ---------------------------------------------------------------- -(see also file CHANGES) +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. + +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". * @@ -40,7 +52,37 @@ Solution: change proj1_sig into projT1 and similarly (compatible with 8.4) * Other detailed changes * -Universe Polymorphism. +(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 |