From 46efe4d675bb96704cf9c598f456a2999b013dbc Mon Sep 17 00:00:00 2001
From: notin
Date: Wed, 4 Feb 2009 16:00:38 +0000
Subject: Fix d'un bug avec l'option gallina

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

diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index f460cfb12c..1480624a50 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -290,7 +290,7 @@ let commands =
   | ("Hypothesis" | "Hypotheses")
   | "End"
 
-let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
+let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
 
 let extraction = 
   "Extraction"
@@ -393,7 +393,8 @@ rule coq_bol = parse
 	if not (!in_proof && !Cdglobals.gallina) then 
 	  begin backtrack lexbuf; body_bol lexbuf end 
 	else
-	  skip_to_dot lexbuf 
+	  let eol = skip_to_dot lexbuf in
+	    if eol then Output.line_break (); eol
       in
 	in_proof := false;
 	if eol then coq_bol lexbuf else coq lexbuf }
@@ -492,7 +493,8 @@ and coq = parse
 	if not (!in_proof && !Cdglobals.gallina) then 
 	  begin backtrack lexbuf; body lexbuf end 
 	else
-	  skip_to_dot lexbuf 
+	  let eol = skip_to_dot lexbuf in
+	    if eol then Output.line_break (); eol
       in
 	in_proof := false;
 	if eol then coq_bol lexbuf else coq lexbuf }
@@ -513,8 +515,7 @@ and coq = parse
 	  if not !Cdglobals.gallina then 
 	    begin backtrack lexbuf; body lexbuf end 
 	  else 
-	    let eol = skip_to_dot lexbuf in
-	      if eol then Output.line_break (); eol
+	    skip_to_dot lexbuf
 	in 
 	  if eol then coq_bol lexbuf else coq lexbuf}
       
-- 
cgit v1.2.3