diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 18:17:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 18:17:04 +0100 |
| commit | d7691de7184b4cdcfd48fd762011569cde5523c5 (patch) | |
| tree | 9c9e14226b070fc2a5cf4c216c4f8c634de20855 /COMPATIBILITY | |
| parent | eed12bddc3e6f6f9192c909a8b8f82859080f3a1 (diff) | |
| parent | aed3c876d422f4dcc0296fd4949148c697f37b1d (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index eeb0c292b..2b3862eb0 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -62,6 +62,13 @@ Type classes. 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 export" or "Qed export ident, .., ident". + Potential sources of incompatibilities between Coq V8.3 and V8.4 ---------------------------------------------------------------- |