diff options
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 34 |
1 files changed, 31 insertions, 3 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index 55b2d003f7..883b8576d2 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -1,8 +1,6 @@ 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". * @@ -40,7 +38,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 |