From e0c8d21414aed1fd96210d153ad85540e03fef42 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 14 Mar 2018 19:36:47 +0100
Subject: [Sphinx] Move chapter 13 to new infrastructure

---
 doc/refman/Reference-Manual.tex | 1 -
 1 file changed, 1 deletion(-)

(limited to 'doc/refman/Reference-Manual.tex')

diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 9545a47c9b..357272aa4e 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)
-- 
cgit v1.2.3