aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-15 10:30:31 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-15 10:38:52 +0100
commitdb282f831cbf619e417593c602de24960c3ca69c (patch)
tree6f4bcc1830e37713c571e58084214571c8920ff1 /doc/stdlib
parentf439001caa24671d03d8816964ceb8e483660e70 (diff)
parentce395ca02311bbe6ecc1b2782e74312272dd15ec (diff)
Merge branch 'v8.5'
Diffstat (limited to 'doc/stdlib')
-rw-r--r--doc/stdlib/index-list.html.template1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 33de399c0..a8bbdeb37 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -618,6 +618,7 @@ through the <tt>Require Import</tt> command.</p>
Compatibility wrappers for previous versions of Coq
</dt>
<dd>
+ theories/Compat/AdmitAxiom.v
theories/Compat/Coq84.v
theories/Compat/Coq85.v
</dd>