aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-12-14 11:22:54 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-12-14 11:22:54 +0100
commit81ef6a6dc1bfc3db0e7df3e32b6446fc4d2c4008 (patch)
treed8f4d554a78bca6901cbc63e7f6af8dbc40462e6 /doc/stdlib
parent9329cb508f336b48a2bf2e699886546158b6b4d8 (diff)
Moved proof_admitted to its own file, named "AdmitAxiom.v".
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 866193ffb..292b2b36c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -617,6 +617,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>