1 files changed, 86 insertions, 1 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY
index eaeb2cba..d423e71d 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,9 +1,94 @@
+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)
 
-Universe Polymorphism.
+- 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