aboutsummaryrefslogtreecommitdiff
path: root/ChangeLog
diff options
context:
space:
mode:
authorCyril Cohen2018-10-26 03:32:24 +0200
committerGitHub2018-10-26 03:32:24 +0200
commit76fb3c00580488f75362153f6ea252f9b4d4084b (patch)
treefb69783f75d4044edfe97e5b4edf134022094d33 /ChangeLog
parent277b8f6f419e9a699fbcbe97d5c13ec81a1e7199 (diff)
parenta974272fbdb5d121a4ac3e47a716d7406f8571b9 (diff)
Merge pull request #218 from CohenCyril/tagged
removing multiple definitions of [tT]ag*
Diffstat (limited to 'ChangeLog')
-rw-r--r--ChangeLog3
1 files changed, 3 insertions, 0 deletions
diff --git a/ChangeLog b/ChangeLog
index a9650bc..2e8a495 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -11,6 +11,9 @@
`all_iffLR` and coercion `all_iffP` (see header for doc)
proved by circular implication P0 -> P1 -> ... -> Pn -> P0
+ * Removed duplicated definitions of `tag` `tagged` and `Tagged`
+ from eqtype.v. They were already in ssrfun.v.
+
24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7
* Added compatibility with Coq 8.8 and lost compatibility with