diff options
| author | notin | 2009-02-04 16:00:38 +0000 |
|---|---|---|
| committer | notin | 2009-02-04 16:00:38 +0000 |
| commit | 46efe4d675bb96704cf9c598f456a2999b013dbc (patch) | |
| tree | 4762f773ccbb23c4d07099f501495550b377f66a /tools | |
| parent | 3bb0fa9596316e2a049df646e08bafbffc9691ad (diff) | |
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
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/pretty.mll | 11 |
1 files 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} |