Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg

8 files changed, 189 insertions, 71 deletions

diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 98457261..eb3a19fa 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_makefile.ml4 11883 2009-02-06 09:54:52Z herbelin $ *)
+(* $Id: coq_makefile.ml4 12176 2009-06-09 09:44:40Z notin $ *)
 
 (* créer un Makefile pour un développement Coq automatiquement *)
 
@@ -212,7 +212,7 @@ let clean sds sps =
   print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \
          $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n";
   if !some_mlfile then
-    print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n";
+    print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o)\n";
   if Coq_config.has_natdynlink && !some_mlfile then
     print "\trm -f $(CMXSFILES) $(CMXSFILES:.cmxs=.o)\n";
   print "\t- rm -rf html\n";
@@ -243,14 +243,14 @@ let footer_includes () =
 let implicit () =
   let ml_rules () =
     print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n";
-    print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n";
-    print "%.cmxs: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n";
+    print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+    print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+    print "%.cmxs: %.ml\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n";
     print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
-    print "%.cmxs: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n";
+    print "%.cmxs: %.ml4\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n";
     print "%.ml.d: %.ml\n";
-    print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(PP) \"$<\" > \"$@\"\n\n"
+    print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(OCAMLLIBS) $(PP) \"$<\" > \"$@\"\n\n"
   and v_rule () =
     print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n";
     print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
@@ -283,8 +283,8 @@ let variables defs =
     print "COQDOC:=$(COQBIN)coqdoc\n";
     print "COQMKTOP:=$(COQBIN)coqmktop\n";
     (* Caml executables and relative variables *)
-    printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
-    printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
+    printf "CAMLC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlc;
+    printf "CAMLOPTC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlopt;
     printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
     printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
     print "GRAMMARS:=grammar.cma\n";
@@ -315,7 +315,7 @@ let include_dirs (inc_i,inc_r) =
   let str_i' = parse_includes inc_i' in
   let str_r = parse_rec_includes inc_r in
     section "Libraries definitions.";
-    print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n  " str_i; print "\n";
+    print "OCAMLLIBS:="; print_list "\\\n  " str_i; print "\n";
     print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\
   -I $(COQLIB)/library -I $(COQLIB)/parsing \\
   -I $(COQLIB)/pretyping -I $(COQLIB)/interp \\
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5bcbed64..b3f0739d 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -54,9 +54,10 @@ let toc = ref false
 let page_title = ref ""
 let title = ref ""
 let externals = ref true
-let coqlib = ref "http://coq.inria.fr/library/"
+let coqlib = ref Coq_config.wwwstdlib
 let coqlib_path = ref Coq_config.coqlib
 let raw_comments = ref false
+let parse_comments = ref false
 let interpolate = ref false
 
 let charset = ref "iso-8859-1"
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index a9a99706..762be5af 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -57,6 +57,11 @@ body { padding: 0px 0px;
     display: inline;
     font-family: monospace } 
 
+.comment { 
+    display: inline;
+    font-family: monospace;
+    color: red; } 
+
 .code { 
     display: block;
     font-family: monospace } 
@@ -80,18 +85,46 @@ body { padding: 0px 0px;
     color: rgb(40%,0%,40%);
 }
 
+.id[type="variable"] { 
+    color: rgb(40%,0%,40%);
+}
+
 .id[type="definition"] { 
     color: rgb(0%,40%,0%);
 }
 
+.id[type="abbreviation"] { 
+    color: rgb(0%,40%,0%);
+}
+
 .id[type="lemma"] { 
     color: rgb(0%,40%,0%);
 }
 
+.id[type="instance"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="projection"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="method"] { 
+    color: rgb(0%,40%,0%);
+}
+
 .id[type="inductive"] { 
     color: rgb(0%,0%,80%);
 }
 
+.id[type="record"] { 
+    color: rgb(0%,0%,80%);
+}
+
+.id[type="class"] { 
+    color: rgb(0%,0%,80%);
+}
+
 .id[type="keyword"] { 
  color : #cf1d1d;
 /*     color: black; */
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index ef4f4119..fca9a1d7 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -70,6 +70,9 @@
 % !!! CAUTION: This environment may have empty contents
 \newenvironment{coqdoccode}{}{}
 
+% Environment for comments
+\newenvironment{coqdoccomment}{\tt(*}{*)}
+
 % newline and indentation 
 %BEGIN LATEX
 % Base indentation length
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 2e97618b..2ee9ac96 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml 11828 2009-01-22 06:44:11Z notin $ i*)
+(*i $Id: main.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
@@ -56,7 +56,7 @@ let usage () =
   prerr_endline "  --verbose            verbose mode";  
   prerr_endline "  --no-externals       no links to Coq standard library";
   prerr_endline "  --coqlib <url>       set URL for Coq standard library";
-  prerr_endline "                       (default is http://coq.inria.fr/library/)";
+  prerr_endline ("                       (default is " ^ Coq_config.wwwstdlib ^ ")");
   prerr_endline "  --boot               run in boot mode";
   prerr_endline "  --coqlib_path <dir>  set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>    map physical dir to Coq dir";
@@ -65,6 +65,7 @@ let usage () =
   prerr_endline "  --charset <string>   set HTML charset";
   prerr_endline "  --inputenc <string>  set LaTeX input encoding";
   prerr_endline "  --interpolate        try to typeset identifiers in comments using definitions in the same module";
+  prerr_endline "  --parse-comments     parse regular comments";
   prerr_endline "";
   exit 1
 
@@ -273,6 +274,8 @@ let parse () =
 	usage ()
     | ("-raw-comments" | "--raw-comments") :: rem ->
 	Cdglobals.raw_comments := true; parse_rec rem
+    | ("-parse-comments" | "--parse-comments") :: rem ->
+	Cdglobals.parse_comments := true; parse_rec rem
     | ("-interpolate" | "--interpolate") :: rem ->
 	Cdglobals.interpolate := true; parse_rec rem
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index c146150c..1ad8b14f 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 11823 2009-01-21 15:32:37Z msozeau $ i*)
+(*i $Id: output.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 open Cdglobals
 open Index
@@ -292,13 +292,13 @@ module Latex = struct
 
   let ident s l = 
     if !in_title then (
-      printf "\\texorpdfstring{";
+      printf "\\texorpdfstring{\\protect";
       with_latex_printing (fun s -> ident s l) s;
       printf "}{"; raw_ident s; printf "}")
     else
       with_latex_printing (fun s -> ident s l) s
     
-  let symbol = with_latex_printing raw_ident
+  let symbol s = with_latex_printing raw_ident s
 
   let rec reach_item_level n = 
     if !item_level < n then begin
@@ -320,6 +320,12 @@ module Latex = struct
 
   let end_doc () = in_doc := false; stop_item ()
 
+  let comment c = char c
+
+  let start_comment () = printf "\\begin{coqdoccomment}\n"
+
+  let end_comment () = printf "\\end{coqdoccomment}\n"
+
   let start_coq () = printf "\\begin{coqdoccode}\n"
 
   let end_coq () = printf "\\end{coqdoccode}\n"
@@ -389,8 +395,6 @@ module Html = struct
 	  printf "<div id=\"main\">\n\n"
 	end
 
-  let self = "http://coq.inria.fr"
-
   let trailer () =
     if !index && !current_module <> "Index" then 
       printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
@@ -406,7 +410,7 @@ module Html = struct
       else
 	begin
 	  printf "<hr/>This page has been generated by ";
-	  printf "<a href=\"%s\">coqdoc</a>\n" self;
+	  printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
 	  printf "</div>\n\n</div>\n\n</body>\n</html>"
 	end
 
@@ -456,14 +460,15 @@ module Html = struct
   let ident_ref m fid typ s =
     match find_module m with
     | Local ->
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
 	printf "<span class=\"id\" type=\"%s\">" typ; 
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s;
-	printf "</a></span>"
+	raw_ident s;
+	printf "</span></a>"
     | Coqlib when !externals ->
 	let m = Filename.concat !coqlib m in
-	  printf "<span class=\"id\" type=\"%s\">" typ; 
 	  printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
-	  raw_ident s; printf "</a></span>"
+	  printf "<span class=\"id\" type=\"%s\">" typ; 
+	  raw_ident s; printf "</span></a>"
     | Coqlib | Unknown ->
 	printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
 	  
@@ -477,8 +482,9 @@ module Html = struct
 	try
 	  (match Index.find !current_module loc with
 	     | Def (fullid,ty) -> 
+		 printf "<a name=\"%s\">" fullid; 
 		 printf "<span class=\"id\" type=\"%s\">" (type_name ty); 
-		 printf "<a name=\"%s\">" fullid; raw_ident s; printf "</a></span>"
+		 raw_ident s; printf "</span></a>"
              | Mod (m,s') when s = s' ->
 		 module_ref m s
 	     | Ref (m,fullid,ty) -> 
@@ -500,9 +506,11 @@ module Html = struct
     with Not_found -> 
       f tok
 
-  let ident s l = with_html_printing (fun s -> ident s l) s
+  let ident s l =
+    with_html_printing (fun s -> ident s l) s
 
-  let symbol = with_html_printing raw_ident
+  let symbol s =
+    with_html_printing raw_ident s
 
   let rec reach_item_level n = 
     if !item_level < n then begin
@@ -532,6 +540,10 @@ module Html = struct
     stop_item (); 
     if not !raw_comments then printf "\n</div>\n"
 
+  let start_comment () = printf "<span class=\"comment\">(*"
+
+  let end_comment () = printf "*)</span>"
+
   let start_code () = end_doc (); start_coq ()
 
   let end_code () = end_coq (); start_doc ()
@@ -540,7 +552,11 @@ module Html = struct
 
   let end_inline_coq () = printf "</span>"
 
-  let paragraph () = stop_item (); printf "\n<br/><br/>\n"
+  let paragraph () = 
+    let i = !item_level in
+      stop_item ();
+      if i > 0 then printf "\n"
+      else printf "\n<br/> <br/>\n"
 
   let section lev f =
     let lab = new_label () in
@@ -770,6 +786,9 @@ module TeXmacs = struct
 
   let end_coq () = ()
 
+  let start_comment () = ()
+  let end_comment () = ()
+
   let start_code () = in_doc := true; printf "<\\code>\n"
   let end_code () = in_doc := false; printf "\n</code>"
 
@@ -849,7 +868,7 @@ module Raw = struct
 
   let ident s loc = raw_ident s
 
-  let symbol = raw_ident
+  let symbol s = raw_ident s
 
   let item n = printf "- "
 
@@ -858,6 +877,9 @@ module Raw = struct
   let start_doc () = printf "(** "
   let end_doc () = printf " *)\n"
 
+  let start_comment () = ()
+  let end_comment () = ()
+
   let start_coq () = ()
   let end_coq () = ()
 
@@ -911,6 +933,9 @@ let start_module =
 let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc
 let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.end_doc
 
+let start_comment = select Latex.start_comment Html.start_comment TeXmacs.start_comment Raw.start_comment
+let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment Raw.end_comment
+
 let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq
 let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq
 
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 3da80335..75c7ccf8 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: output.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 open Cdglobals
 open Index
@@ -28,6 +28,9 @@ val start_module : unit -> unit
 val start_doc : unit -> unit
 val end_doc : unit -> unit
 
+val start_comment : unit -> unit
+val end_comment : unit -> unit
+
 val start_coq : unit -> unit
 val end_coq : unit -> unit
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 3ae5cbed..c4a1a76f 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 11823 2009-01-21 15:32:37Z msozeau $ i*)
+(*i $Id: pretty.mll 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -57,7 +57,7 @@
   let formatted = ref false
   let brackets = ref 0
   let comment_level = ref 0
-  let in_proof = ref false
+  let in_proof = ref None
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
 
@@ -162,6 +162,8 @@
     else
       String.sub s 1 (String.length s - 3)
 
+  let symbol lexbuf s = Output.symbol s 
+
 }
 
 (*s Regular expressions *)
@@ -217,7 +219,10 @@ let thm_token =
   | "Proposition" 
   | "Property"
   | "Goal"
-  | "Next" space+ "Obligation"
+
+let prf_token =
+  "Next" space+ "Obligation"
+  | "Proof" (space* "." | space+ "with")
 
 let def_token = 
   "Definition" 
@@ -290,7 +295,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"
@@ -307,7 +312,6 @@ let prog_kw =
 
 let gallina_kw_to_hide =
     "Implicit" space+ "Arguments"
-  | "Next" "Obligation"
   | "Ltac"
   | "Require"
   | "Import"
@@ -343,7 +347,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 
 rule coq_bol = parse
   | space* nl+
-      { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf }
+      { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
   | space* "(**" space_nl
       { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
@@ -379,27 +383,29 @@ rule coq_bol = parse
 	  Output.indentation nbsp;
 	  Output.ident s (lexeme_start lexbuf + isp); 
 	  let eol = body lexbuf in
-	    in_proof := true;
+	    in_proof := Some eol;
 	    if eol then coq_bol lexbuf else coq lexbuf }
-  | space* "Proof" (space* "." | space+ "with")
-      { in_proof := true;
+  | space* prf_token
+      { in_proof := Some true;
 	let eol = 
-	if not !Cdglobals.gallina then 
-	  begin backtrack lexbuf; body_bol lexbuf end 
-	else true
+	  if not !Cdglobals.gallina then 
+	    begin backtrack lexbuf; body_bol lexbuf end 
+	  else 
+	    let s = lexeme lexbuf in
+	      if s.[String.length s - 1] = '.' then false
+	      else skip_to_dot lexbuf
 	in if eol then coq_bol lexbuf else coq lexbuf }
   | space* end_kw { 
       let eol = 
-	if not (!in_proof && !Cdglobals.gallina) then 
+	if not (!in_proof <> None && !Cdglobals.gallina) then 
 	  begin backtrack lexbuf; body_bol lexbuf end 
-	else
-	  skip_to_dot lexbuf 
+	else skip_to_dot lexbuf
       in
-	in_proof := false;
+	in_proof := None;
 	if eol then coq_bol lexbuf else coq lexbuf }
   | space* gallina_kw
       { 
-	in_proof := false;
+	in_proof := None;
 	let s = lexeme lexbuf in 
 	let nbsp,isp = count_spaces s in
 	let s = String.sub s isp (String.length s - isp)  in
@@ -409,7 +415,7 @@ rule coq_bol = parse
 	    if eol then coq_bol lexbuf else coq lexbuf }
   | space* prog_kw
       { 
-	in_proof := false;
+	in_proof := None;
 	let s = lexeme lexbuf in 
 	let nbsp,isp = count_spaces s in
 	  Output.indentation nbsp;
@@ -441,6 +447,12 @@ rule coq_bol = parse
 	coq_bol lexbuf }
   | space* "(*"
       { comment_level := 1; 
+	if !Cdglobals.parse_comments then begin
+	  let s = lexeme lexbuf in 
+	  let nbsp,isp = count_spaces s in
+	    Output.indentation nbsp;
+	    Output.start_comment ();
+	end;
 	let eol = comment lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | eof 
@@ -458,7 +470,7 @@ rule coq_bol = parse
 
 and coq = parse
   | nl 
-      { if not (!in_proof && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
+      { if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
   | "(**" space_nl
       { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
@@ -466,12 +478,18 @@ and coq = parse
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | "(*"
       { comment_level := 1;
+	if !Cdglobals.parse_comments then begin
+	  let s = lexeme lexbuf in 
+	  let nbsp,isp = count_spaces s in
+	    Output.indentation nbsp;
+	    Output.start_comment ();
+	end;
 	let eol = comment lexbuf in
-	  if eol then begin Output.line_break(); coq_bol lexbuf end 
+	  if eol then coq_bol lexbuf
           else coq lexbuf
       }
   | nl+ space* "]]"
-      { if not !formatted then begin Output.symbol (lexeme lexbuf); coq lexbuf end }
+      { if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end }
   | eof 
       { () }
   | gallina_kw_to_hide
@@ -487,14 +505,29 @@ and coq = parse
 	      let eol=body lexbuf in 
 		if eol then coq_bol lexbuf else coq lexbuf
 	    end }
+  | prf_token
+      { let eol = 
+	  if not !Cdglobals.gallina then 
+	    begin backtrack lexbuf; body_bol lexbuf end 
+	  else 
+	    let s = lexeme lexbuf in
+	    let eol = 
+	      if s.[String.length s - 1] = '.' then false
+	      else skip_to_dot lexbuf
+	    in
+	      eol
+	in if eol then coq_bol lexbuf else coq lexbuf }
   | end_kw { 
       let eol = 
-	if not (!in_proof && !Cdglobals.gallina) then 
+	if not !Cdglobals.gallina then 
 	  begin backtrack lexbuf; body lexbuf end 
-	else
-	  skip_to_dot lexbuf 
+	else 
+	  let eol = skip_to_dot lexbuf in
+	    if !in_proof <> Some true && eol then 
+	      Output.line_break ();
+	    eol
       in
-	in_proof := false;
+	in_proof := None;
 	if eol then coq_bol lexbuf else coq lexbuf }
   | gallina_kw
       { let s = lexeme lexbuf in 
@@ -513,8 +546,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}
       
@@ -616,8 +648,7 @@ and escaped_coq = parse
       { () }
   | token_brackets
       { let s = lexeme lexbuf in
-	Output.symbol s;
-	escaped_coq lexbuf }
+	  symbol lexbuf s; escaped_coq lexbuf }
   | (identifier '.')* identifier
       { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
   | _ 
@@ -644,15 +675,30 @@ and comments = parse
 (*s Skip comments *)
 
 and comment = parse
-  | "(*" { incr comment_level; comment lexbuf }
-  | "*)" space* nl { decr comment_level; if !comment_level > 0 then comment lexbuf else true }
-  | "*)" { decr comment_level; if !comment_level > 0 then comment lexbuf else false }
-  | eof  {  false }
-  | _    {  comment lexbuf }
-
+  | "(*" { incr comment_level;
+	   if !Cdglobals.parse_comments then Output.start_comment ();
+	   comment lexbuf }
+  | "*)" space* nl {
+      if !Cdglobals.parse_comments then	(Output.end_comment (); Output.line_break ());
+      decr comment_level; if !comment_level > 0 then comment lexbuf else true }
+  | "*)" { 
+      if !Cdglobals.parse_comments then (Output.end_comment ());
+      decr comment_level; if !comment_level > 0 then comment lexbuf else false }
+  | "[" { 
+      if !Cdglobals.parse_comments then (
+	brackets := 1;
+	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ());
+      comment lexbuf }
+  | eof  { false }
+  | space+ { if !Cdglobals.parse_comments then 
+	Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf }
+  | nl   { if !Cdglobals.parse_comments then Output.line_break (); comment lexbuf }
+  | _    { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
+  comment lexbuf }
+      
 and skip_to_dot = parse
   | '.' space* nl { true }
-  | eof | '.' space+ { false}
+  | eof | '.' space+ { false }
   | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
   | _ { skip_to_dot lexbuf }
 
@@ -664,15 +710,19 @@ and body_bol = parse
 and body = parse
   | nl {Output.line_break(); body_bol lexbuf}
   | nl+ space* "]]"
-      { if not !formatted then begin Output.symbol (lexeme lexbuf); body lexbuf end else true }
+      { if not !formatted then begin symbol lexbuf (lexeme lexbuf); body lexbuf end else true }
   | eof { false }
-  | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }      
-  | '.' space+ { Output.char '.'; Output.char ' '; false }
+  | '.' space* nl | '.' space* eof 
+	{ Output.char '.'; Output.line_break(); 
+	  if not !formatted then true else body_bol lexbuf }      
+  | '.' space+ { Output.char '.'; Output.char ' '; 
+	  if not !formatted then false else body lexbuf }
   | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
   | "(*" { comment_level := 1; 
+	   if !Cdglobals.parse_comments then Output.start_comment ();
 	   let eol = comment lexbuf in 
 	     if eol 
-	     then begin Output.line_break(); body_bol lexbuf end
+	     then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
 	     else body lexbuf }
   | identifier 
       { let s = lexeme lexbuf in 
@@ -680,7 +730,7 @@ and body = parse
 	  body lexbuf }
   | token_no_brackets
       { let s = lexeme lexbuf in
-	  Output.symbol s; body lexbuf }
+	  symbol lexbuf s; body lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
 	  Output.char c; 
           body lexbuf }
@@ -695,7 +745,7 @@ and notation = parse
   | '"' { Output.char '"'}
   | token
       { let s = lexeme lexbuf in
-	  Output.symbol s; notation lexbuf }
+	  symbol lexbuf s; notation lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
 	  Output.char c; 
           notation lexbuf }