diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-27 11:28:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-28 17:47:03 +0200 |
| commit | 2c8335b4d2cf928f8494b4abf100b5bb6a8d2fa0 (patch) | |
| tree | a908ef721a2c004ccae577db39b9afd910a25f62 /COMPATIBILITY | |
| parent | db8ffccb25f763d193a63dbe65ff079619a3780e (diff) | |
Updating CHANGES w.r.t. opacity in type inference + layout of file.
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index 33bb1d30e..57553f9e1 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -19,6 +19,11 @@ Universe Polymorphism. 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. + Potential sources of incompatibilities between Coq V8.3 and V8.4 ---------------------------------------------------------------- |