From ca7a7ffbf5e0576e2a50052e644c1d067843fddf Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 3 Apr 2018 14:05:50 +0200
Subject: [Sphinx] Move chapter 7 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 e511160075..8909c0fefd 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -99,7 +99,6 @@ Options A and B of the licence are {\em not} elected.}
 
 \part{The proof engine}
 \include{RefMan-oth.v}% Vernacular commands
-\include{RefMan-pro.v}% Proof handling
 \include{RefMan-ltac.v}% Writing tactics
 
 \lstset{language=SSR}
-- 
cgit v1.2.3