From da882cfdac822da8d53e8c11b4a890e1643901ad Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 1 Dec 2009 16:36:52 +0000
Subject: Fix make_exact_entry to allow applying [forall x, P x] hints
 directly, avoiding the introduction of eta-redexes. Prioritize hints over
 intros in typeclass resolution to profit from that. Add a minor fix in coqdoc
 by F. Garillot.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12550 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coqdoc/cpretty.mll | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 4742a2e5dd..4f1406cc83 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -184,10 +184,10 @@
   let check_start_list str =
     let n_dashes = count_dashes str in
     let (n_spaces,_) = count_spaces str in
-      if n_dashes >= 4 then
+      if n_dashes >= 4 && not !Cdglobals.plain_comments then
         Rule
       else
-        if n_dashes = 1 then
+        if n_dashes = 1 && not !Cdglobals.plain_comments then
           List n_spaces
         else
           Neither
-- 
cgit v1.2.3