From 1681238424c2d46e7a31467212d4daed4b30a827 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 13 Jun 2014 17:04:05 +0200
Subject: Deprecate useless option -quality.

---
 man/coqtop.1 | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'man')

diff --git a/man/coqtop.1 b/man/coqtop.1
index 8006d4993..33982b117 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -168,11 +168,6 @@ export XML files either to the hierarchy rooted in
 the directory $COQ_XML_LIBRARY_ROOT (if set) or to
 stdout (if unset)
 
-.TP
-.B \-quality
-improve the legibility of the proof terms produced by
-some tactics
-
 .SH SEE ALSO
 
 .BR coqc (1),
-- 
cgit v1.2.3