diff options
| author | Maxime Dénès | 2017-05-20 01:34:36 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-20 01:34:36 +0200 |
| commit | b7cf93cec115b61889e31c0abefdbd29d9b51ebe (patch) | |
| tree | 8cc84e9c2ae8de301e10d8ea3f2d12303dfb126b /COMPATIBILITY | |
| parent | 7dc84057e3596b1c3f6ec869daebcfa8747f5c12 (diff) | |
| parent | 741f3fab052b91eaec57f32b639ca722c3d8dc34 (diff) | |
Merge PR#474: A fix for #5390 (a useful error on used introduction names was masked).
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index d423e71df3..78dfabaa3e 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -1,3 +1,10 @@ +Potential sources of incompatibilities between Coq V8.6 and V8.7 +---------------------------------------------------------------- + +- Extra superfluous names in introduction patterns may now raise an + error rather than a warning when the superfluous name is already in + use. The easy fix is to remove the superfluous name. + Potential sources of incompatibilities between Coq V8.5 and V8.6 ---------------------------------------------------------------- |