aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
diff options
context:
space:
mode:
authorJason Gross2018-10-02 16:14:20 -0400
committerVincent Laporte2019-04-02 11:55:51 +0000
commitb1162463d577baf450c3f33ab880e7d9afe21148 (patch)
treed85438c47e85ebda6cbccab94daf5d312c502e44 /doc/stdlib
parent974dc811fe30a762235b68fb3c0ac5c3eeca45b9 (diff)
Remove -compat 8.7
This removes various compatibility notations. Closes #8374 This commit was mostly created by running `./dev/tools/update-compat.py --release`. There's a bit of manual spacing adjustment around all of the removed compatibility notations, and some test-suite updates were done manually. The update to CHANGES.md was manual.
Diffstat (limited to 'doc/stdlib')
-rw-r--r--doc/stdlib/index-list.html.template1
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index fd79996bb7..a561de1d0c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -619,7 +619,6 @@ through the <tt>Require Import</tt> command.</p>
</dt>
<dd>
theories/Compat/AdmitAxiom.v
- theories/Compat/Coq87.v
theories/Compat/Coq88.v
theories/Compat/Coq89.v
theories/Compat/Coq810.v