aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.doc2
-rw-r--r--doc/refman/Reference-Manual.tex1
-rw-r--r--doc/sphinx/user-extensions/proof-schemes.rst (renamed from doc/refman/RefMan-sch.tex)0
3 files changed, 1 insertions, 2 deletions
diff --git a/Makefile.doc b/Makefile.doc
index 64b43f5ea..077ae965c 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -60,7 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
RefMan-gal.v.tex \
RefMan-lib.v.tex \
RefMan-oth.v.tex RefMan-ltac.v.tex \
- RefMan-pro.v.tex RefMan-sch.v.tex \
+ RefMan-pro.v.tex \
Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
Setoid.v.tex Classes.v.tex Universes.v.tex \
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 9545a47c9..357272aa4 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -110,7 +110,6 @@ Options A and B of the licence are {\em not} elected.}
\part{User extensions}
%%SUPPRIME \include{RefMan-tus.v}% Writing tactics
-\include{RefMan-sch.v}% The Scheme commands
\part{Practical tools}
\include{RefMan-com}% The coq commands (coqc coqtop)
diff --git a/doc/refman/RefMan-sch.tex b/doc/sphinx/user-extensions/proof-schemes.rst
index 600471123..600471123 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/sphinx/user-extensions/proof-schemes.rst