aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/index.html
diff options
context:
space:
mode:
authorMaxime Dénès2018-04-16 18:16:37 +0200
committerMaxime Dénès2018-04-16 18:16:37 +0200
commit72c35b310a7b8a23934a1e9632d4d989c184d0d7 (patch)
tree41182461fb1fc1d626dcb717e675a7ccb9fa656f /doc/refman/index.html
parent3e7863e9369d38537685576a8642dbe0c062d0c5 (diff)
Remove LaTeX refman, now that migration to Sphinx is complete
Diffstat (limited to 'doc/refman/index.html')
-rw-r--r--doc/refman/index.html14
1 files changed, 0 insertions, 14 deletions
diff --git a/doc/refman/index.html b/doc/refman/index.html
deleted file mode 100644
index b937350e6e..0000000000
--- a/doc/refman/index.html
+++ /dev/null
@@ -1,14 +0,0 @@
-<HTML>
-
-<HEAD>
-
-<TITLE>The Coq Proof Assistant Reference Manual</TITLE>
-
-</HEAD>
-
-<FRAMESET ROWS=90%,*>
- <FRAME SRC="cover.html" NAME="UP">
- <FRAME SRC="menu.html">
-</FRAMESET>
-
-</HTML>