r8620@thot: notin | 2006-03-08 11:44:16 +0100

 Modifications diverses de Coqdoc:
   - modification du comportement par défaut de l'option --latex
   - ajout d'une option --stdout
   - réaménagement dans les sources (création de global.ml)
   - modification du parser de coqdoc pour regler les problèmes liés à 
     la syntaxe V8.
   - Correction du bug #1052 sur les commentaires en fin de ligne
 


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8617 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 633 insertions, 620 deletions

diff --git a/.depend b/.depend
index d28fbd358c..5b2ecb8be4 100644
--- a/.depend
+++ b/.depend
@@ -54,12 +54,12 @@ kernel/indtypes.cmi: kernel/univ.cmi kernel/typeops.cmi kernel/term.cmi \
     kernel/declarations.cmi 
 kernel/inductive.cmi: kernel/univ.cmi kernel/term.cmi kernel/names.cmi \
     kernel/environ.cmi kernel/declarations.cmi 
-kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi 
-kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \
-    kernel/declarations.cmi 
 kernel/modops.cmi: lib/util.cmi kernel/univ.cmi kernel/names.cmi \
     kernel/mod_subst.cmi kernel/environ.cmi kernel/entries.cmi \
     kernel/declarations.cmi 
+kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi 
+kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \
+    kernel/declarations.cmi 
 kernel/names.cmi: lib/predicate.cmi lib/pp.cmi 
 kernel/pre_env.cmi: lib/util.cmi kernel/univ.cmi kernel/term.cmi \
     kernel/sign.cmi kernel/names.cmi kernel/declarations.cmi 
@@ -85,9 +85,6 @@ kernel/vm.cmi: kernel/term.cmi kernel/names.cmi kernel/cemitcodes.cmi \
     kernel/cbytecodes.cmi 
 lib/bigint.cmi: lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
-lib/rtree.cmi: lib/pp.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi lib/compat.cmo 
 library/declare.cmi: kernel/term.cmi kernel/sign.cmi kernel/safe_typing.cmi \
     library/nametab.cmi kernel/names.cmi library/libnames.cmi \
     kernel/indtypes.cmi kernel/environ.cmi kernel/entries.cmi \
@@ -118,6 +115,9 @@ library/library.cmi: lib/util.cmi lib/system.cmi lib/pp.cmi kernel/names.cmi \
 library/nameops.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi 
 library/nametab.cmi: lib/util.cmi lib/pp.cmi kernel/names.cmi \
     library/libnames.cmi 
+lib/rtree.cmi: lib/pp.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi lib/compat.cmo 
 parsing/egrammar.cmi: toplevel/vernacexpr.cmo lib/util.cmi \
     interp/topconstr.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \
     interp/ppextend.cmi parsing/pcoq.cmi kernel/names.cmi \
@@ -347,11 +347,11 @@ toplevel/record.cmi: toplevel/vernacexpr.cmo interp/topconstr.cmi \
 toplevel/searchisos.cmi: kernel/term.cmi kernel/names.cmi \
     library/libobject.cmi 
 toplevel/toplevel.cmi: lib/pp.cmi parsing/pcoq.cmi 
-toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi 
 toplevel/vernacentries.cmi: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
     interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \
     library/libnames.cmi pretyping/evd.cmi kernel/environ.cmi 
 toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
+toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi 
 toplevel/whelp.cmi: interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \
     kernel/environ.cmi 
 contrib/cc/ccalgo.cmi: lib/util.cmi kernel/term.cmi lib/pp.cmi \
@@ -360,9 +360,9 @@ contrib/cc/ccproof.cmi: kernel/names.cmi contrib/cc/ccalgo.cmi
 contrib/cc/cctac.cmi: kernel/term.cmi proofs/proof_type.cmi 
 contrib/correctness/past.cmi: lib/util.cmi interp/topconstr.cmi \
     kernel/term.cmi kernel/names.cmi 
-contrib/correctness/pcic.cmi: pretyping/rawterm.cmi 
 contrib/correctness/pcicenv.cmi: kernel/term.cmi kernel/sign.cmi \
     kernel/names.cmi 
+contrib/correctness/pcic.cmi: pretyping/rawterm.cmi 
 contrib/correctness/pdb.cmi: kernel/names.cmi 
 contrib/correctness/peffect.cmi: lib/pp.cmi kernel/names.cmi 
 contrib/correctness/penv.cmi: kernel/term.cmi kernel/names.cmi \
@@ -382,8 +382,8 @@ contrib/correctness/ptyping.cmi: interp/topconstr.cmi kernel/term.cmi \
     kernel/names.cmi 
 contrib/correctness/putil.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi 
 contrib/correctness/pwp.cmi: kernel/term.cmi 
-contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi 
 contrib/dp/dp_cvcl.cmi: contrib/dp/fol.cmi 
+contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi 
 contrib/dp/dp_simplify.cmi: contrib/dp/fol.cmi 
 contrib/dp/dp_sorts.cmi: contrib/dp/fol.cmi 
 contrib/dp/dp_zenon.cmi: contrib/dp/fol.cmi 
@@ -427,10 +427,10 @@ contrib/first-order/unify.cmi: kernel/term.cmi
 contrib/funind/indfun_common.cmi: kernel/term.cmi pretyping/rawterm.cmi \
     lib/pp.cmi kernel/names.cmi library/libnames.cmi 
 contrib/funind/new_arg_principle.cmi: proofs/tacmach.cmi kernel/names.cmi 
-contrib/funind/rawterm_to_relation.cmi: interp/topconstr.cmi \
-    pretyping/rawterm.cmi kernel/names.cmi 
 contrib/funind/rawtermops.cmi: lib/util.cmi pretyping/rawterm.cmi \
     kernel/names.cmi library/libnames.cmi 
+contrib/funind/rawterm_to_relation.cmi: interp/topconstr.cmi \
+    pretyping/rawterm.cmi kernel/names.cmi 
 contrib/funind/tacinvutils.cmi: lib/util.cmi pretyping/termops.cmi \
     kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
     proofs/tacmach.cmi tactics/tacinterp.cmi tactics/refine.cmi \
@@ -471,8 +471,9 @@ contrib/xml/xmlcommand.cmi: contrib/xml/xml.cmi kernel/term.cmi \
     proofs/proof_type.cmi contrib/xml/proof2aproof.cmo library/libnames.cmi \
     pretyping/evd.cmi contrib/xml/acic.cmo 
 ide/utils/configwin.cmi: ide/utils/uoptions.cmi 
-tools/coqdoc/output.cmi: tools/coqdoc/index.cmi 
-tools/coqdoc/pretty.cmi: tools/coqdoc/index.cmi 
+tools/coqdoc/index.cmi: tools/coqdoc/cdglobals.cmo 
+tools/coqdoc/output.cmi: tools/coqdoc/index.cmi tools/coqdoc/cdglobals.cmo 
+tools/coqdoc/pretty.cmi: tools/coqdoc/index.cmi tools/coqdoc/cdglobals.cmo 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 dev/db_printers.cmo: lib/pp.cmi kernel/names.cmi 
@@ -511,6 +512,14 @@ ide/config_lexer.cmo: lib/util.cmi ide/config_parser.cmi
 ide/config_lexer.cmx: lib/util.cmx ide/config_parser.cmx 
 ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi 
 ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi 
+ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \
+    lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \
+    ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \
+    ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi 
+ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \
+    lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \
+    ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \
+    ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi 
 ide/coq.cmo: toplevel/vernacexpr.cmo toplevel/vernacentries.cmi \
     toplevel/vernac.cmi lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
     proofs/tacmach.cmi tactics/tacinterp.cmi library/states.cmi \
@@ -535,14 +544,6 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \
     ide/coq.cmi 
 ide/coq_tactics.cmo: ide/coq_tactics.cmi 
 ide/coq_tactics.cmx: ide/coq_tactics.cmi 
-ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \
-    lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \
-    ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \
-    ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi 
-ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \
-    lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \
-    ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \
-    ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi 
 ide/find_phrase.cmo: ide/ideutils.cmi 
 ide/find_phrase.cmx: ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmi 
@@ -721,6 +722,14 @@ kernel/inductive.cmo: lib/util.cmi kernel/univ.cmi kernel/type_errors.cmi \
 kernel/inductive.cmx: lib/util.cmx kernel/univ.cmx kernel/type_errors.cmx \
     kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx kernel/names.cmx \
     kernel/environ.cmx kernel/declarations.cmx kernel/inductive.cmi 
+kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \
+    kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \
+    kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \
+    kernel/modops.cmi 
+kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \
+    kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \
+    kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \
+    kernel/modops.cmi 
 kernel/mod_subst.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi \
     kernel/names.cmi kernel/mod_subst.cmi 
 kernel/mod_subst.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx \
@@ -735,14 +744,6 @@ kernel/mod_typing.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \
     kernel/names.cmx kernel/modops.cmx kernel/mod_subst.cmx \
     kernel/environ.cmx kernel/entries.cmx kernel/declarations.cmx \
     kernel/cemitcodes.cmx kernel/mod_typing.cmi 
-kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \
-    kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \
-    kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \
-    kernel/modops.cmi 
-kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \
-    kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \
-    kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \
-    kernel/modops.cmi 
 kernel/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/hashcons.cmi \
     kernel/names.cmi 
 kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/hashcons.cmx \
@@ -841,10 +842,10 @@ lib/edit.cmo: lib/util.cmi lib/pp.cmi lib/bstack.cmi lib/edit.cmi
 lib/edit.cmx: lib/util.cmx lib/pp.cmx lib/bstack.cmx lib/edit.cmi 
 lib/explore.cmo: lib/explore.cmi 
 lib/explore.cmx: lib/explore.cmi 
-lib/gmap.cmo: lib/gmap.cmi 
-lib/gmap.cmx: lib/gmap.cmi 
 lib/gmapl.cmo: lib/util.cmi lib/gmap.cmi lib/gmapl.cmi 
 lib/gmapl.cmx: lib/util.cmx lib/gmap.cmx lib/gmapl.cmi 
+lib/gmap.cmo: lib/gmap.cmi 
+lib/gmap.cmx: lib/gmap.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
@@ -853,26 +854,14 @@ lib/heap.cmo: lib/heap.cmi
 lib/heap.cmx: lib/heap.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/pp_control.cmo: lib/pp_control.cmi 
 lib/pp_control.cmx: lib/pp_control.cmi 
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/predicate.cmo: lib/predicate.cmi 
 lib/predicate.cmx: lib/predicate.cmi 
 lib/profile.cmo: lib/profile.cmi 
 lib/profile.cmx: lib/profile.cmi 
-lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi 
-lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi 
-lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi 
-library/decl_kinds.cmo: lib/util.cmi 
-library/decl_kinds.cmx: lib/util.cmx 
 library/declare.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \
     kernel/type_errors.cmi kernel/term.cmi library/summary.cmi \
     kernel/sign.cmi kernel/safe_typing.cmi kernel/reduction.cmi lib/pp.cmi \
@@ -905,6 +894,8 @@ library/declaremods.cmx: lib/util.cmx library/summary.cmx \
     library/libobject.cmx library/libnames.cmx library/lib.cmx \
     library/global.cmx kernel/environ.cmx kernel/entries.cmx \
     kernel/declarations.cmx library/declaremods.cmi 
+library/decl_kinds.cmo: lib/util.cmi 
+library/decl_kinds.cmx: lib/util.cmx 
 library/dischargedhypsmap.cmo: lib/util.cmi kernel/term.cmi \
     library/summary.cmi kernel/reduction.cmi library/nametab.cmi \
     kernel/names.cmi library/libobject.cmi library/libnames.cmi \
@@ -987,6 +978,16 @@ library/states.cmx: lib/system.cmx library/summary.cmx library/library.cmx \
     library/lib.cmx library/states.cmi 
 library/summary.cmo: lib/util.cmi lib/pp.cmi lib/dyn.cmi library/summary.cmi 
 library/summary.cmx: lib/util.cmx lib/pp.cmx lib/dyn.cmx library/summary.cmi 
+lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi 
+lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi 
+lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi 
 parsing/argextend.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     parsing/q_util.cmi parsing/q_coqast.cmo parsing/pcoq.cmi \
     interp/genarg.cmi 
@@ -2247,16 +2248,6 @@ toplevel/toplevel.cmx: toplevel/vernacexpr.cmx toplevel/vernac.cmx \
     toplevel/toplevel.cmi 
 toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi 
 toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi 
-toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
-    toplevel/vernacentries.cmi lib/util.cmi lib/system.cmi library/states.cmi \
-    parsing/ppvernac.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \
-    lib/options.cmi kernel/names.cmi library/library.cmi library/lib.cmi \
-    parsing/lexer.cmi interp/constrintern.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
-    toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \
-    parsing/ppvernac.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \
-    lib/options.cmx kernel/names.cmx library/library.cmx library/lib.cmx \
-    parsing/lexer.cmx interp/constrintern.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: kernel/vm.cmi toplevel/vernacinterp.cmi \
     toplevel/vernacexpr.cmo kernel/vconv.cmi lib/util.cmi kernel/univ.cmi \
     kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
@@ -2317,6 +2308,16 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/proof_type.cmx lib/pp.cmx \
     lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \
     toplevel/vernacinterp.cmi 
+toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacentries.cmi lib/util.cmi lib/system.cmi library/states.cmi \
+    parsing/ppvernac.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \
+    lib/options.cmi kernel/names.cmi library/library.cmi library/lib.cmi \
+    parsing/lexer.cmi interp/constrintern.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \
+    parsing/ppvernac.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \
+    lib/options.cmx kernel/names.cmx library/library.cmx library/lib.cmx \
+    parsing/lexer.cmx interp/constrintern.cmx toplevel/vernac.cmi 
 toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi lib/system.cmi \
     interp/syntax_def.cmi proofs/refiner.cmi pretyping/rawterm.cmi lib/pp.cmi \
@@ -2367,6 +2368,12 @@ contrib/cc/g_congruence.cmx: lib/util.cmx tactics/tactics.cmx \
     proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \
     interp/genarg.cmx parsing/egrammar.cmx toplevel/cerrors.cmx \
     contrib/cc/cctac.cmx 
+contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \
+    kernel/sign.cmi kernel/names.cmi library/global.cmi \
+    contrib/correctness/pcicenv.cmi 
+contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \
+    kernel/sign.cmx kernel/names.cmx library/global.cmx \
+    contrib/correctness/pcicenv.cmi 
 contrib/correctness/pcic.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
     kernel/term.cmi kernel/sign.cmi toplevel/record.cmi pretyping/rawterm.cmi \
@@ -2381,12 +2388,6 @@ contrib/correctness/pcic.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     library/libnames.cmx kernel/indtypes.cmx library/global.cmx \
     kernel/entries.cmx pretyping/detyping.cmx library/declare.cmx \
     kernel/declarations.cmx contrib/correctness/pcic.cmi 
-contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \
-    kernel/sign.cmi kernel/names.cmi library/global.cmi \
-    contrib/correctness/pcicenv.cmi 
-contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \
-    kernel/sign.cmx kernel/names.cmx library/global.cmx \
-    contrib/correctness/pcicenv.cmi 
 contrib/correctness/pdb.cmo: pretyping/termops.cmi kernel/term.cmi \
     library/nametab.cmi kernel/names.cmi library/global.cmi \
     interp/constrintern.cmi contrib/correctness/pdb.cmi 
@@ -2507,6 +2508,8 @@ contrib/correctness/pwp.cmx: lib/util.cmx pretyping/termops.cmx \
     library/nametab.cmx kernel/names.cmx library/libnames.cmx \
     tactics/hipattern.cmx library/global.cmx kernel/environ.cmx \
     contrib/correctness/pwp.cmi 
+contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi 
+contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi 
 contrib/dp/dp.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \
     kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
     proofs/tacmach.cmi library/summary.cmi pretyping/reductionops.cmi \
@@ -2523,8 +2526,6 @@ contrib/dp/dp.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \
     library/global.cmx contrib/dp/fol.cmi pretyping/evd.cmx \
     kernel/environ.cmx contrib/dp/dp_why.cmx kernel/declarations.cmx \
     interp/coqlib.cmx contrib/dp/dp.cmi 
-contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi 
-contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi 
 contrib/dp/dp_simplify.cmo: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi 
 contrib/dp/dp_simplify.cmx: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi 
 contrib/dp/dp_sorts.cmo: contrib/dp/fol.cmi contrib/dp/dp_sorts.cmi 
@@ -2801,24 +2802,6 @@ contrib/fourier/g_fourier.cmx: lib/util.cmx tactics/tacinterp.cmx \
     proofs/tacexpr.cmx proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx \
     parsing/pcoq.cmx contrib/fourier/fourierR.cmx parsing/egrammar.cmx \
     toplevel/cerrors.cmx 
-contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
-    interp/topconstr.cmi kernel/term.cmi proofs/tacmach.cmi \
-    library/states.cmi contrib/recdef/recdef.cmo \
-    contrib/funind/rawterm_to_relation.cmi pretyping/rawterm.cmi lib/pp.cmi \
-    lib/options.cmi interp/notation.cmi contrib/funind/new_arg_principle.cmi \
-    kernel/names.cmi library/libnames.cmi pretyping/indrec.cmi \
-    contrib/funind/indfun_common.cmi library/impargs.cmi library/global.cmi \
-    pretyping/evd.cmi kernel/environ.cmi library/decl_kinds.cmo \
-    interp/constrintern.cmi toplevel/command.cmi 
-contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
-    interp/topconstr.cmx kernel/term.cmx proofs/tacmach.cmx \
-    library/states.cmx contrib/recdef/recdef.cmx \
-    contrib/funind/rawterm_to_relation.cmx pretyping/rawterm.cmx lib/pp.cmx \
-    lib/options.cmx interp/notation.cmx contrib/funind/new_arg_principle.cmx \
-    kernel/names.cmx library/libnames.cmx pretyping/indrec.cmx \
-    contrib/funind/indfun_common.cmx library/impargs.cmx library/global.cmx \
-    pretyping/evd.cmx kernel/environ.cmx library/decl_kinds.cmx \
-    interp/constrintern.cmx toplevel/command.cmx 
 contrib/funind/indfun_common.cmo: lib/util.cmi pretyping/termops.cmi \
     kernel/term.cmi pretyping/rawterm.cmi lib/pp.cmi library/nametab.cmi \
     kernel/names.cmi library/libnames.cmi library/global.cmi \
@@ -2849,6 +2832,24 @@ contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     contrib/funind/indfun.cmx tactics/hiddentac.cmx library/global.cmx \
     interp/genarg.cmx parsing/egrammar.cmx kernel/declarations.cmx \
     toplevel/cerrors.cmx 
+contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
+    interp/topconstr.cmi kernel/term.cmi proofs/tacmach.cmi \
+    library/states.cmi contrib/recdef/recdef.cmo \
+    contrib/funind/rawterm_to_relation.cmi pretyping/rawterm.cmi lib/pp.cmi \
+    lib/options.cmi interp/notation.cmi contrib/funind/new_arg_principle.cmi \
+    kernel/names.cmi library/libnames.cmi pretyping/indrec.cmi \
+    contrib/funind/indfun_common.cmi library/impargs.cmi library/global.cmi \
+    pretyping/evd.cmi kernel/environ.cmi library/decl_kinds.cmo \
+    interp/constrintern.cmi toplevel/command.cmi 
+contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
+    interp/topconstr.cmx kernel/term.cmx proofs/tacmach.cmx \
+    library/states.cmx contrib/recdef/recdef.cmx \
+    contrib/funind/rawterm_to_relation.cmx pretyping/rawterm.cmx lib/pp.cmx \
+    lib/options.cmx interp/notation.cmx contrib/funind/new_arg_principle.cmx \
+    kernel/names.cmx library/libnames.cmx pretyping/indrec.cmx \
+    contrib/funind/indfun_common.cmx library/impargs.cmx library/global.cmx \
+    pretyping/evd.cmx kernel/environ.cmx library/decl_kinds.cmx \
+    interp/constrintern.cmx toplevel/command.cmx 
 contrib/funind/invfun.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \
     tactics/tacticals.cmi proofs/tacmach.cmi contrib/funind/tacinvutils.cmi \
     kernel/sign.cmi pretyping/rawterm.cmi lib/pp.cmi kernel/names.cmi \
@@ -2893,6 +2894,18 @@ contrib/funind/new_arg_principle.cmx: toplevel/vernacexpr.cmx \
     toplevel/command.cmx kernel/closure.cmx pretyping/clenv.cmx \
     toplevel/cerrors.cmx contrib/cc/cctac.cmx \
     contrib/funind/new_arg_principle.cmi 
+contrib/funind/rawtermops.cmo: lib/util.cmi proofs/tactic_debug.cmi \
+    tactics/tacinterp.cmi pretyping/rawterm.cmi parsing/printer.cmi \
+    parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \
+    library/libnames.cmi pretyping/inductiveops.cmi \
+    contrib/funind/indfun_common.cmi library/global.cmi pretyping/evd.cmi \
+    interp/coqlib.cmi contrib/funind/rawtermops.cmi 
+contrib/funind/rawtermops.cmx: lib/util.cmx proofs/tactic_debug.cmx \
+    tactics/tacinterp.cmx pretyping/rawterm.cmx parsing/printer.cmx \
+    parsing/ppconstr.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \
+    library/libnames.cmx pretyping/inductiveops.cmx \
+    contrib/funind/indfun_common.cmx library/global.cmx pretyping/evd.cmx \
+    interp/coqlib.cmx contrib/funind/rawtermops.cmi 
 contrib/funind/rawterm_to_relation.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     interp/topconstr.cmi kernel/term.cmi contrib/funind/rawtermops.cmi \
     pretyping/rawterm.cmi parsing/printer.cmi parsing/ppvernac.cmi lib/pp.cmi \
@@ -2907,18 +2920,6 @@ contrib/funind/rawterm_to_relation.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     contrib/funind/indfun_common.cmx library/impargs.cmx interp/coqlib.cmx \
     interp/constrextern.cmx toplevel/command.cmx toplevel/cerrors.cmx \
     contrib/funind/rawterm_to_relation.cmi 
-contrib/funind/rawtermops.cmo: lib/util.cmi proofs/tactic_debug.cmi \
-    tactics/tacinterp.cmi pretyping/rawterm.cmi parsing/printer.cmi \
-    parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \
-    library/libnames.cmi pretyping/inductiveops.cmi \
-    contrib/funind/indfun_common.cmi library/global.cmi pretyping/evd.cmi \
-    interp/coqlib.cmi contrib/funind/rawtermops.cmi 
-contrib/funind/rawtermops.cmx: lib/util.cmx proofs/tactic_debug.cmx \
-    tactics/tacinterp.cmx pretyping/rawterm.cmx parsing/printer.cmx \
-    parsing/ppconstr.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \
-    library/libnames.cmx pretyping/inductiveops.cmx \
-    contrib/funind/indfun_common.cmx library/global.cmx pretyping/evd.cmx \
-    interp/coqlib.cmx contrib/funind/rawtermops.cmi 
 contrib/funind/tacinv.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \
     tactics/tactics.cmi tactics/tacticals.cmi pretyping/tacred.cmi \
@@ -3115,6 +3116,14 @@ contrib/interface/pbp.cmx: lib/util.cmx pretyping/typing.cmx \
     proofs/logic.cmx library/libnames.cmx tactics/hipattern.cmx \
     library/global.cmx interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
     interp/coqlib.cmx contrib/interface/pbp.cmi 
+contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \
+    contrib/interface/vtp.cmi contrib/interface/translate.cmi \
+    parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \
+    contrib/interface/ascent.cmi 
+contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \
+    contrib/interface/vtp.cmx contrib/interface/translate.cmx \
+    parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \
+    contrib/interface/ascent.cmi 
 contrib/interface/showproof.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/typing.cmi contrib/interface/translate.cmi \
     pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi \
@@ -3137,14 +3146,6 @@ contrib/interface/showproof.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
     kernel/declarations.cmx interp/constrintern.cmx pretyping/clenv.cmx \
     contrib/interface/showproof.cmi 
-contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \
-    contrib/interface/vtp.cmi contrib/interface/translate.cmi \
-    parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \
-    contrib/interface/ascent.cmi 
-contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \
-    contrib/interface/vtp.cmx contrib/interface/translate.cmx \
-    parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \
-    contrib/interface/ascent.cmi 
 contrib/interface/translate.cmo: contrib/interface/xlate.cmi \
     contrib/interface/vtp.cmi toplevel/vernacinterp.cmi lib/util.cmi \
     kernel/term.cmi proofs/tacmach.cmi kernel/sign.cmi proofs/proof_type.cmi \
@@ -3419,6 +3420,30 @@ contrib/subtac/g_eterm.cmx: lib/util.cmx proofs/tacmach.cmx \
     tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/refiner.cmx \
     parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx contrib/subtac/eterm.cmx \
     parsing/egrammar.cmx toplevel/cerrors.cmx 
+contrib/subtac/interp_fixpoint.cmo: lib/util.cmi kernel/typeops.cmi \
+    kernel/type_errors.cmi interp/topconstr.cmi pretyping/termops.cmi \
+    kernel/term.cmi contrib/subtac/subtac_errors.cmo \
+    contrib/subtac/subtac_coercion.cmo kernel/sign.cmi \
+    contrib/subtac/scoq.cmo pretyping/reductionops.cmi \
+    pretyping/recordops.cmi pretyping/rawterm.cmi parsing/printer.cmi \
+    pretyping/pretype_errors.cmi parsing/ppconstr.cmi lib/pp.cmi \
+    pretyping/pattern.cmi kernel/names.cmi library/nameops.cmi \
+    library/libnames.cmi library/global.cmi pretyping/evd.cmi \
+    pretyping/evarutil.cmi pretyping/evarconv.cmi contrib/subtac/eterm.cmi \
+    kernel/environ.cmi lib/dyn.cmi interp/coqlib.cmi \
+    contrib/subtac/context.cmo pretyping/classops.cmi 
+contrib/subtac/interp_fixpoint.cmx: lib/util.cmx kernel/typeops.cmx \
+    kernel/type_errors.cmx interp/topconstr.cmx pretyping/termops.cmx \
+    kernel/term.cmx contrib/subtac/subtac_errors.cmx \
+    contrib/subtac/subtac_coercion.cmx kernel/sign.cmx \
+    contrib/subtac/scoq.cmx pretyping/reductionops.cmx \
+    pretyping/recordops.cmx pretyping/rawterm.cmx parsing/printer.cmx \
+    pretyping/pretype_errors.cmx parsing/ppconstr.cmx lib/pp.cmx \
+    pretyping/pattern.cmx kernel/names.cmx library/nameops.cmx \
+    library/libnames.cmx library/global.cmx pretyping/evd.cmx \
+    pretyping/evarutil.cmx pretyping/evarconv.cmx contrib/subtac/eterm.cmx \
+    kernel/environ.cmx lib/dyn.cmx interp/coqlib.cmx \
+    contrib/subtac/context.cmx pretyping/classops.cmx 
 contrib/subtac/interp.cmo: lib/util.cmi kernel/typeops.cmi \
     kernel/type_errors.cmi interp/topconstr.cmi pretyping/termops.cmi \
     kernel/term.cmi contrib/subtac/subtac_errors.cmo \
@@ -3449,30 +3474,6 @@ contrib/subtac/interp.cmx: lib/util.cmx kernel/typeops.cmx \
     lib/dyn.cmx kernel/declarations.cmx library/decl_kinds.cmx \
     interp/coqlib.cmx contrib/subtac/context.cmx interp/constrintern.cmx \
     toplevel/command.cmx pretyping/classops.cmx pretyping/cases.cmx 
-contrib/subtac/interp_fixpoint.cmo: lib/util.cmi kernel/typeops.cmi \
-    kernel/type_errors.cmi interp/topconstr.cmi pretyping/termops.cmi \
-    kernel/term.cmi contrib/subtac/subtac_errors.cmo \
-    contrib/subtac/subtac_coercion.cmo kernel/sign.cmi \
-    contrib/subtac/scoq.cmo pretyping/reductionops.cmi \
-    pretyping/recordops.cmi pretyping/rawterm.cmi parsing/printer.cmi \
-    pretyping/pretype_errors.cmi parsing/ppconstr.cmi lib/pp.cmi \
-    pretyping/pattern.cmi kernel/names.cmi library/nameops.cmi \
-    library/libnames.cmi library/global.cmi pretyping/evd.cmi \
-    pretyping/evarutil.cmi pretyping/evarconv.cmi contrib/subtac/eterm.cmi \
-    kernel/environ.cmi lib/dyn.cmi interp/coqlib.cmi \
-    contrib/subtac/context.cmo pretyping/classops.cmi 
-contrib/subtac/interp_fixpoint.cmx: lib/util.cmx kernel/typeops.cmx \
-    kernel/type_errors.cmx interp/topconstr.cmx pretyping/termops.cmx \
-    kernel/term.cmx contrib/subtac/subtac_errors.cmx \
-    contrib/subtac/subtac_coercion.cmx kernel/sign.cmx \
-    contrib/subtac/scoq.cmx pretyping/reductionops.cmx \
-    pretyping/recordops.cmx pretyping/rawterm.cmx parsing/printer.cmx \
-    pretyping/pretype_errors.cmx parsing/ppconstr.cmx lib/pp.cmx \
-    pretyping/pattern.cmx kernel/names.cmx library/nameops.cmx \
-    library/libnames.cmx library/global.cmx pretyping/evd.cmx \
-    pretyping/evarutil.cmx pretyping/evarconv.cmx contrib/subtac/eterm.cmx \
-    kernel/environ.cmx lib/dyn.cmx interp/coqlib.cmx \
-    contrib/subtac/context.cmx pretyping/classops.cmx 
 contrib/subtac/scoq.cmo: lib/util.cmi interp/topconstr.cmi \
     pretyping/termops.cmi kernel/term.cmi parsing/printer.cmi \
     pretyping/pretype_errors.cmi lib/pp.cmi kernel/names.cmi \
@@ -3497,6 +3498,24 @@ contrib/subtac/sparser.cmx: toplevel/vernacinterp.cmx \
     kernel/names.cmx library/nameops.cmx library/libnames.cmx \
     contrib/subtac/interp.cmx interp/genarg.cmx kernel/environ.cmx \
     parsing/egrammar.cmx toplevel/cerrors.cmx 
+contrib/subtac/subtac_coercion.cmo: lib/util.cmi kernel/typeops.cmi \
+    kernel/term.cmi contrib/subtac/subtac_errors.cmo contrib/subtac/scoq.cmo \
+    pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
+    pretyping/recordops.cmi pretyping/rawterm.cmi parsing/printer.cmi \
+    pretyping/pretype_errors.cmi lib/pp.cmi kernel/names.cmi \
+    library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
+    pretyping/evarconv.cmi contrib/subtac/eterm.cmi kernel/environ.cmi \
+    interp/coqlib.cmi contrib/subtac/context.cmo pretyping/classops.cmi 
+contrib/subtac/subtac_coercion.cmx: lib/util.cmx kernel/typeops.cmx \
+    kernel/term.cmx contrib/subtac/subtac_errors.cmx contrib/subtac/scoq.cmx \
+    pretyping/retyping.cmx pretyping/reductionops.cmx kernel/reduction.cmx \
+    pretyping/recordops.cmx pretyping/rawterm.cmx parsing/printer.cmx \
+    pretyping/pretype_errors.cmx lib/pp.cmx kernel/names.cmx \
+    library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
+    pretyping/evarconv.cmx contrib/subtac/eterm.cmx kernel/environ.cmx \
+    interp/coqlib.cmx contrib/subtac/context.cmx pretyping/classops.cmx 
+contrib/subtac/subtac_errors.cmo: lib/util.cmi parsing/printer.cmi lib/pp.cmi 
+contrib/subtac/subtac_errors.cmx: lib/util.cmx parsing/printer.cmx lib/pp.cmx 
 contrib/subtac/subtac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     kernel/typeops.cmi kernel/type_errors.cmi pretyping/termops.cmi \
     kernel/term.cmi contrib/subtac/subtac_errors.cmo \
@@ -3527,36 +3546,12 @@ contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     kernel/environ.cmx lib/dyn.cmx interp/coqlib.cmx \
     contrib/subtac/context.cmx toplevel/command.cmx pretyping/classops.cmx \
     toplevel/cerrors.cmx 
-contrib/subtac/subtac_coercion.cmo: lib/util.cmi kernel/typeops.cmi \
-    kernel/term.cmi contrib/subtac/subtac_errors.cmo contrib/subtac/scoq.cmo \
-    pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
-    pretyping/recordops.cmi pretyping/rawterm.cmi parsing/printer.cmi \
-    pretyping/pretype_errors.cmi lib/pp.cmi kernel/names.cmi \
-    library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
-    pretyping/evarconv.cmi contrib/subtac/eterm.cmi kernel/environ.cmi \
-    interp/coqlib.cmi contrib/subtac/context.cmo pretyping/classops.cmi 
-contrib/subtac/subtac_coercion.cmx: lib/util.cmx kernel/typeops.cmx \
-    kernel/term.cmx contrib/subtac/subtac_errors.cmx contrib/subtac/scoq.cmx \
-    pretyping/retyping.cmx pretyping/reductionops.cmx kernel/reduction.cmx \
-    pretyping/recordops.cmx pretyping/rawterm.cmx parsing/printer.cmx \
-    pretyping/pretype_errors.cmx lib/pp.cmx kernel/names.cmx \
-    library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
-    pretyping/evarconv.cmx contrib/subtac/eterm.cmx kernel/environ.cmx \
-    interp/coqlib.cmx contrib/subtac/context.cmx pretyping/classops.cmx 
-contrib/subtac/subtac_errors.cmo: lib/util.cmi parsing/printer.cmi lib/pp.cmi 
-contrib/subtac/subtac_errors.cmx: lib/util.cmx parsing/printer.cmx lib/pp.cmx 
-contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi 
-contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx 
 contrib/xml/acic2Xml.cmo: contrib/xml/xml.cmi lib/util.cmi kernel/term.cmi \
     kernel/names.cmi contrib/xml/cic2acic.cmo contrib/xml/acic.cmo 
 contrib/xml/acic2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx kernel/term.cmx \
     kernel/names.cmx contrib/xml/cic2acic.cmx contrib/xml/acic.cmx 
-contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \
-    tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \
-    contrib/xml/acic.cmo 
-contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \
-    tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \
-    contrib/xml/acic.cmx 
+contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi 
+contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx 
 contrib/xml/cic2acic.cmo: lib/util.cmi contrib/xml/unshare.cmi \
     kernel/univ.cmi pretyping/termops.cmi kernel/term.cmi \
     pretyping/reductionops.cmi parsing/printer.cmi lib/pp.cmi \
@@ -3575,6 +3570,12 @@ contrib/xml/cic2acic.cmx: lib/util.cmx contrib/xml/unshare.cmx \
     kernel/environ.cmx contrib/xml/doubleTypeInference.cmx \
     library/dischargedhypsmap.cmx library/declare.cmx kernel/declarations.cmx \
     contrib/xml/acic.cmx 
+contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \
+    tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \
+    contrib/xml/acic.cmo 
+contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \
+    tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \
+    contrib/xml/acic.cmx 
 contrib/xml/doubleTypeInference.cmo: lib/util.cmi contrib/xml/unshare.cmi \
     kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \
     pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
@@ -3615,8 +3616,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx \
     contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx contrib/xml/acic.cmx 
 contrib/xml/unshare.cmo: contrib/xml/unshare.cmi 
 contrib/xml/unshare.cmx: contrib/xml/unshare.cmi 
-contrib/xml/xml.cmo: contrib/xml/xml.cmi 
-contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: contrib/xml/xml.cmi toplevel/vernac.cmi \
     lib/util.cmi contrib/xml/unshare.cmi kernel/term.cmi proofs/tacmach.cmi \
     pretyping/recordops.cmi proofs/proof_trees.cmi \
@@ -3647,10 +3646,8 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \
     toplevel/vernacinterp.cmx lib/util.cmx lib/pp.cmx parsing/pcoq.cmx \
     parsing/lexer.cmx interp/genarg.cmx parsing/extend.cmx \
     parsing/egrammar.cmx toplevel/cerrors.cmx 
-ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \
-    ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi 
-ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \
-    ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi 
+contrib/xml/xml.cmo: contrib/xml/xml.cmi 
+contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 ide/utils/configwin_html_config.cmo: ide/utils/uoptions.cmi \
     ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo \
     ide/utils/configwin_ihm.cmo 
@@ -3661,6 +3658,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/uoptions.cmi ide/utils/okey.cmi \
     ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo 
 ide/utils/configwin_ihm.cmx: ide/utils/uoptions.cmx ide/utils/okey.cmx \
     ide/utils/configwin_types.cmx ide/utils/configwin_messages.cmx 
+ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \
+    ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi 
+ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \
+    ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi 
 ide/utils/configwin_types.cmo: ide/utils/uoptions.cmi \
     ide/utils/configwin_keys.cmo 
 ide/utils/configwin_types.cmx: ide/utils/uoptions.cmx \
@@ -3671,18 +3672,22 @@ ide/utils/uoptions.cmo: ide/utils/uoptions.cmi
 ide/utils/uoptions.cmx: ide/utils/uoptions.cmi 
 tools/coqdoc/alpha.cmo: tools/coqdoc/alpha.cmi 
 tools/coqdoc/alpha.cmx: tools/coqdoc/alpha.cmi 
-tools/coqdoc/index.cmo: tools/coqdoc/alpha.cmi tools/coqdoc/index.cmi 
-tools/coqdoc/index.cmx: tools/coqdoc/alpha.cmx tools/coqdoc/index.cmi 
+tools/coqdoc/index.cmo: tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmi \
+    tools/coqdoc/index.cmi 
+tools/coqdoc/index.cmx: tools/coqdoc/cdglobals.cmx tools/coqdoc/alpha.cmx \
+    tools/coqdoc/index.cmi 
 tools/coqdoc/main.cmo: tools/coqdoc/pretty.cmi tools/coqdoc/output.cmi \
-    tools/coqdoc/index.cmi config/coq_config.cmi 
+    tools/coqdoc/index.cmi config/coq_config.cmi tools/coqdoc/cdglobals.cmo 
 tools/coqdoc/main.cmx: tools/coqdoc/pretty.cmx tools/coqdoc/output.cmx \
-    tools/coqdoc/index.cmx config/coq_config.cmx 
-tools/coqdoc/output.cmo: tools/coqdoc/index.cmi tools/coqdoc/output.cmi 
-tools/coqdoc/output.cmx: tools/coqdoc/index.cmx tools/coqdoc/output.cmi 
+    tools/coqdoc/index.cmx config/coq_config.cmx tools/coqdoc/cdglobals.cmx 
+tools/coqdoc/output.cmo: tools/coqdoc/index.cmi tools/coqdoc/cdglobals.cmo \
+    tools/coqdoc/output.cmi 
+tools/coqdoc/output.cmx: tools/coqdoc/index.cmx tools/coqdoc/cdglobals.cmx \
+    tools/coqdoc/output.cmi 
 tools/coqdoc/pretty.cmo: tools/coqdoc/output.cmi tools/coqdoc/index.cmi \
-    tools/coqdoc/pretty.cmi 
+    tools/coqdoc/cdglobals.cmo tools/coqdoc/pretty.cmi 
 tools/coqdoc/pretty.cmx: tools/coqdoc/output.cmx tools/coqdoc/index.cmx \
-    tools/coqdoc/pretty.cmi 
+    tools/coqdoc/cdglobals.cmx tools/coqdoc/pretty.cmi 
 tactics/tauto.cmo: parsing/grammar.cma
 tactics/tauto.cmx: parsing/grammar.cma
 tactics/eqdecide.cmo: parsing/grammar.cma
@@ -3786,102 +3791,74 @@ tools/coq_makefile.cmx:
 tools/coq-tex.cmo: 
 tools/coq-tex.cmx: 
 coq_fix_code.o: kernel/byterun/coq_fix_code.c \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
+  /usr/lib/ocaml/3.09.1/caml/config.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/config.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h
 coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/alloc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h \
   kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/alloc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h
 coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
-  kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_values.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h
 coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
+  /usr/lib/ocaml/3.09.1/caml/config.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/config.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h
 coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/alloc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h \
   kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/alloc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h
 coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
-  kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_values.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h
diff --git a/Makefile b/Makefile
index c7e91cd5ae..97122d438c 100644
--- a/Makefile
+++ b/Makefile
@@ -1115,9 +1115,9 @@ $(COQWC): tools/coqwc.cmo
 
 beforedepend:: tools/coqdoc/pretty.ml tools/coqdoc/index.ml
 
-COQDOCCMO=$(CONFIG) tools/coqdoc/alpha.cmo tools/coqdoc/index.cmo \
-          tools/coqdoc/output.cmo tools/coqdoc/pretty.cmo \
-	  tools/coqdoc/main.cmo
+COQDOCCMO=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \
+	tools/coqdoc/index.cmo tools/coqdoc/output.cmo \
+	tools/coqdoc/pretty.cmo tools/coqdoc/main.cmo
 
 $(COQDOC): $(COQDOCCMO)
 	$(SHOW)'OCAMLC -o $@'
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
new file mode 100644
index 0000000000..b5a4cb22cf
--- /dev/null
+++ b/tools/coqdoc/cdglobals.ml
@@ -0,0 +1,72 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+
+
+(*s Output options *)
+
+type target_language = LaTeX | HTML | TeXmacs
+
+let target_language = ref HTML
+
+type output_t =
+  | StdOut
+  | MultFiles
+  | File of string
+
+let output_dir = ref ""
+
+let out_to = ref MultFiles
+
+let out_channel = ref stdout
+
+let open_out_file f =
+  let f = if !output_dir <> "" then Filename.concat !output_dir f else f in
+    out_channel := open_out f
+
+let close_out_file () = close_out !out_channel
+
+
+let header_trailer = ref true
+let quiet = ref false
+let light = ref false
+let gallina = ref false
+let short = ref false
+let index = ref true
+let multi_index = ref false
+let toc = ref false
+let page_title = ref ""
+let title = ref ""
+let externals = ref true
+let coqlib = ref "http://coq.inria.fr/library/"
+let raw_comments = ref false
+
+let charset = ref "iso-8859-1"
+let inputenc = ref ""
+let latin1 = ref false
+let utf8 = ref false
+
+let set_latin1 () =
+  charset := "iso-8859-1";
+  inputenc := "latin1";
+  latin1 := true
+
+let set_utf8 () =
+  charset := "utf-8";
+  inputenc := "utf8";
+  utf8 := true
+
+(* Parsing options *)
+
+type coq_module = string
+
+type file =
+  | Vernac_file of string * coq_module
+  | Latex_file of string
+      
+
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 243a3750b9..1af3945708 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-type coq_module = string
+open Cdglobals
 
 type loc = int
 
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index ae19433f93..091372de48 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -14,7 +14,7 @@ open Filename
 open Lexing 
 open Printf
 
-type coq_module = string
+open Cdglobals
 
 type loc = int
 
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 820ad8240d..d43df8d34e 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -18,6 +18,7 @@
  * It may be removed or abbreviated as far as I am concerned.
  *)
 
+open Cdglobals
 open Filename
 open Printf
 open Output
@@ -33,6 +34,7 @@ let usage () =
   prerr_endline "  --texmacs           produce a TeXmacs document";
   prerr_endline "  --dvi               output the DVI";
   prerr_endline "  --ps                output the PostScript";
+  prerr_endline "  --stdout            write output to stdout";
   prerr_endline "  -o <file>           write output in file <file>";
   prerr_endline "  -d <dir>            output files into directory <dir>";
   prerr_endline "  -g                  (gallina) skip proofs";
@@ -71,7 +73,12 @@ let banner () =
   eprintf "This is coqdoc version %s, compiled on %s\n"
     Coq_config.version Coq_config.compile_date;
   flush stderr
-    
+
+let target_full_name f = 
+  let basefile = chop_suffix f ".v" in
+    match !target_language with
+      | HTML -> basefile ^ ".html"
+      | _ -> basefile ^ ".tex"
 
 (*s \textbf{Separation of files.} Files given on the command line are
     separated according to their type, which is determined by their
@@ -232,8 +239,10 @@ let parse () =
 	multi_index := true; parse_rec rem
     | ("-toc" | "--toc" | "--table-of-contents") :: rem ->
 	toc := true; parse_rec rem
+    | ("-stdout" | "--stdout") :: rem ->
+	out_to := StdOut; parse_rec rem
     | ("-o" | "--output") :: f :: rem ->
-	output_file := f; parse_rec rem
+	out_to := File f; parse_rec rem
     | ("-o" | "--output") :: [] -> 
 	usage ()
     | ("-d" | "--directory") :: dir :: rem ->
@@ -251,30 +260,29 @@ let parse () =
     | ("-t" | "-title" | "--title") :: [] ->
 	usage ()
     | ("-latex" | "--latex") :: rem ->
-	Output.target_language := LaTeX; parse_rec rem
+	Cdglobals.target_language := LaTeX; parse_rec rem
     | ("-dvi" | "--dvi") :: rem ->
-	Output.target_language := LaTeX; dvi := true; parse_rec rem
+	Cdglobals.target_language := LaTeX; dvi := true; parse_rec rem
     | ("-ps" | "--ps") :: rem ->
-	Output.target_language := LaTeX; ps := true; parse_rec rem
+	Cdglobals.target_language := LaTeX; ps := true; parse_rec rem
     | ("-html" | "--html") :: rem ->
-	Output.target_language := HTML; parse_rec rem
+	Cdglobals.target_language := HTML; parse_rec rem
     | ("-texmacs" | "--texmacs") :: rem ->
-	Output.target_language := TeXmacs; parse_rec rem
-
+	Cdglobals.target_language := TeXmacs; parse_rec rem
     | ("-charset" | "--charset") :: s :: rem ->
-	Output.charset := s; parse_rec rem
+	Cdglobals.charset := s; parse_rec rem
     | ("-charset" | "--charset") :: [] ->
 	usage ()
     | ("-inputenc" | "--inputenc") :: s :: rem ->
-	Output.inputenc := s; parse_rec rem
+	Cdglobals.inputenc := s; parse_rec rem
     | ("-inputenc" | "--inputenc") :: [] ->
 	usage ()
     | ("-raw-comments" | "--raw-comments") :: rem ->
-	Output.raw_comments := true; parse_rec rem
+	Cdglobals.raw_comments := true; parse_rec rem
     | ("-latin1" | "--latin1") :: rem ->
-	Output.set_latin1 (); parse_rec rem
+	Cdglobals.set_latin1 (); parse_rec rem
     | ("-utf8" | "--utf8") :: rem ->
-	Output.set_utf8 (); parse_rec rem
+	Cdglobals.set_utf8 (); parse_rec rem
 
     | ("-q" | "-quiet" | "--quiet") :: rem ->
 	quiet := true; parse_rec rem
@@ -298,7 +306,6 @@ let parse () =
 	parse_rec rem
     | ("-files" | "--files") :: [] ->
 	usage ()
-
     | "-R" :: path :: log :: rem -> 
 	add_path path log; parse_rec rem
     | "-R" :: ([] | [_]) ->
@@ -308,12 +315,11 @@ let parse () =
     | ("-glob-from" | "--glob-from") :: [] ->
 	usage ()
     | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
-	Output.externals := false; parse_rec rem
+	Cdglobals.externals := false; parse_rec rem
     | ("--coqlib" | "-coqlib") :: u :: rem ->
-	Output.coqlib := u; parse_rec rem
+	Cdglobals.coqlib := u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
-
     | f :: rem -> 
 	add_file (what_file f); parse_rec rem
   in 
@@ -360,52 +366,114 @@ let copy src dst =
   with End_of_file ->
     close_in cin; close_out cout
 
+(*s Functions for generating output files *)
+
+let gen_one_file l =
+  let file = function
+    | Vernac_file (f,m) -> 
+	set_module m; coq_file f m
+    | Latex_file _ -> ()
+  in
+    header ();
+    if !toc then make_toc ();
+    List.iter file l;
+    if !index then make_index();
+    trailer ()
+      
+let gen_mult_files l =
+  let file = function
+    | Vernac_file (f,m) -> 
+	set_module m;
+	let hf = target_full_name f in
+	  open_out_file hf;
+	  header (); 
+	  if !toc then make_toc ();
+	  coq_file f m; 
+	  trailer ();
+	  close_out_file()
+    | Latex_file _ -> ()
+  in
+    List.iter file l;
+    if (!index && !target_language=HTML) then begin
+      open_out_file "index.html"; 
+      page_title := (if !title <> "" then !title else "Index");
+      header (); make_index (); trailer ();
+      close_out_file()
+    end;
+    if (!toc && !target_language=HTML) then begin
+      open_out_file "toc.html"; 
+      page_title := (if !title <> "" then !title else "Table of contents");
+      header ();
+      if !title <> "" then printf "<h1>%s</h1>\n" !title;
+      make_toc (); 
+      trailer ();
+      close_out_file()
+    end 
+      (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
+
+
+let index_module = function
+  | Vernac_file (_,m) -> Index.add_module m
+  | Latex_file _ -> ()
+
+let produce_document l =
+  List.iter index_module l;
+  match !out_to with
+    | StdOut -> 
+	Cdglobals.out_channel := stdout;
+	gen_one_file l
+    | File f ->
+	open_out_file f;
+	gen_one_file l;
+	close_out_file()
+    | MultFiles ->
+	gen_mult_files l
+
 let produce_output fl =
   if not (!dvi || !ps) then begin
-    if !output_file <> "" then set_out_file !output_file;
     produce_document fl
   end else begin
     let texfile = temp_file "coqdoc" ".tex" in
     let basefile = chop_suffix texfile ".tex" in
-    set_out_file texfile;
-    produce_document fl;
-    let command = 
-      let file = basename texfile in
-      let file = 
-	if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
-      in
-      sprintf "(latex %s && latex %s) 1>&2 %s" file file
-	(if !quiet then "> /dev/null" else "")
-    in
-    let res = locally (dirname texfile) Sys.command command in
-    if res <> 0 then begin
-      eprintf "Couldn't run LaTeX successfully\n"; 
-      clean_and_exit basefile res
-    end;
-    let dvifile = basefile ^ ".dvi" in
-    if !dvi then begin
-      if !output_file <> "" then 
-	(* we cannot use Sys.rename accross file systems *)
-	copy dvifile !output_file 
-      else 
-	cat dvifile
-    end;
-    if !ps then begin
-      let psfile = 
-	if !output_file <> "" then !output_file else basefile ^ ".ps" 
-      in
+      open_out_file texfile;
+      produce_document fl;
       let command = 
-	sprintf "dvips %s -o %s %s" dvifile psfile 
-	  (if !quiet then "> /dev/null 2>&1" else "")
+	let file = basename texfile in
+	let file = 
+	  if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
+	in
+	  sprintf "(latex %s && latex %s) 1>&2 %s" file file
+	    (if !quiet then "> /dev/null" else "")
       in
-      let res = Sys.command command in
-      if res <> 0 then begin
-	eprintf "Couldn't run dvips successfully\n"; 
-	clean_and_exit basefile res
-      end;
-      if !output_file = "" then cat psfile
-    end;
-    clean_temp_files basefile
+      let res = locally (dirname texfile) Sys.command command in
+	if res <> 0 then begin
+	  eprintf "Couldn't run LaTeX successfully\n"; 
+	  clean_and_exit basefile res
+	end;
+	let dvifile = basefile ^ ".dvi" in
+	  if !dvi then begin
+	    if !output_file <> "" then 
+	      (* we cannot use Sys.rename accross file systems *)
+	      copy dvifile !output_file 
+	    else 
+	      cat dvifile
+	  end;
+	  if !ps then begin
+	    let psfile = 
+	      if !output_file <> "" then !output_file else basefile ^ ".ps" 
+	    in
+	    let command = 
+	      sprintf "dvips %s -o %s %s" dvifile psfile 
+		(if !quiet then "> /dev/null 2>&1" else "")
+	    in
+	    let res = Sys.command command in
+	      if res <> 0 then begin
+		eprintf "Couldn't run dvips successfully\n"; 
+		clean_and_exit basefile res
+	      end;
+	      if !output_file = "" then cat psfile
+	  end;
+	  clean_temp_files basefile
   end
 
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index c81bbf7a43..fcf83a391a 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -8,28 +8,11 @@
 
 (*i $Id$ i*)
 
+open Cdglobals
 open Index
 
-(*s Target language *)
-
-type target_language = LaTeX | HTML | TeXmacs
-
-let target_language = ref HTML
-
 (*s Low level output *)
 
-let out_channel = ref stdout
-let output_is_file = ref false
-let output_dir = ref ""
-
-let set_out_file f = 
-  let f = if !output_dir <> "" then Filename.concat !output_dir f else f in
-  out_channel := open_out f;
-  output_is_file := true
-
-let close () =
-  if !output_is_file then close_out !out_channel
-
 let output_char c = Pervasives.output_char !out_channel c
 
 let output_string s = Pervasives.output_string !out_channel s
@@ -38,43 +21,6 @@ let printf s = Printf.fprintf !out_channel s
 
 let sprintf = Printf.sprintf
 
-let dump_file f =
-  let ch = open_in f in
-  try
-    while true do
-      Pervasives.output_char !out_channel (input_char ch)
-    done
-  with End_of_file -> close_in ch
-
-(*s Options *)
-
-let header_trailer = ref true
-let quiet = ref false
-let light = ref false
-let short = ref false
-let index = ref true
-let multi_index = ref false
-let toc = ref false
-let page_title = ref ""
-let title = ref ""
-let externals = ref true
-let coqlib = ref "http://coq.inria.fr/library/"
-let raw_comments = ref false
-
-let charset = ref "iso-8859-1"
-let inputenc = ref ""
-let latin1 = ref false
-let utf8 = ref false
-
-let set_latin1 () =
-  charset := "iso-8859-1";
-  inputenc := "latin1";
-  latin1 := true
-
-let set_utf8 () =
-  charset := "utf-8";
-  inputenc := "utf8";
-  utf8 := true
 
 (*s Coq keywords *)
 
@@ -85,9 +31,9 @@ let build_table l =
 
 let is_keyword = 
   build_table
-    [ "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
+    [ "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
       "CoInductive"; "Defined"; "Definition"; 
-      "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint";
+      "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
       "Immediate"; "Implicit"; "Import"; "Inductive"; 
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
@@ -508,14 +454,14 @@ module Html = struct
   let separate_index navig i =
     let idx = i.idx_name in
     let one_letter ((c,l) as cl) =
-      set_out_file (sprintf "index_%s_%c.html" idx c);
+      open_out_file (sprintf "index_%s_%c.html" idx c);
       header ();
       navig ();
       printf "<hr/>";
       letter_index true idx cl;
       if List.length l > 30 then begin printf "<hr/>"; navig () end;
       trailer ();
-      close ()
+      close_out_file ()
     in
     List.iter one_letter i.idx_entries
 
@@ -556,43 +502,26 @@ module Html = struct
     printf "</table>\n"
 
   let make_index () =
-    if !index then begin
-      let idxl = 
-	let glob,bt = Index.all_entries () in
+    let idxl = 
+      let glob,bt = Index.all_entries () in
 	format_global_index glob ::
-	List.map format_bytype_index bt 
-      in
-      let navig () = navig_index idxl in 
-      set_out_file "index.html";
+	  List.map format_bytype_index bt 
+    in
+    let navig () = navig_index idxl in 
       current_module := "Index";
-      page_title := (if !title <> "" then !title else "Index");
-      header ();
+      let one_index i =
+	if i.idx_size > 0 then begin
+	  printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
+	  all_letters i
+	end
+	in
       if !title <> "" then printf "<h1>%s</h1>\n" !title;
       navig ();
-      if !multi_index then begin
-	trailer (); 
-	close ();
-	List.iter (separate_index navig) idxl;
-      end else begin
-	let one_index i =
-	  if i.idx_size > 0 then begin
-	    printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
-	    all_letters i
-	  end
-	in
-	List.iter one_index idxl;
-	printf "<hr/>";
-	navig ();
-	trailer ();
-	close ()
-      end;
-    end
+      List.iter one_index idxl;
+      printf "<hr/>";
+      navig ()
 
   let make_toc () = 
-    set_out_file "toc.html";
-    page_title := (if !title <> "" then !title else "Table of contents");
-    header ();
-    if !title <> "" then printf "<h1>%s</h1>\n" !title;
     let make_toc_entry = function
       | Toc_library m -> 
 	  stop_item ();
@@ -603,9 +532,6 @@ module Html = struct
     in
     Queue.iter make_toc_entry toc_q;
     stop_item ();
-    if !index then printf "<a href=\"index.html\"><h2>Index</h2></a>";
-    trailer ();
-    close ()
 
 end
 
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index dd38dd68f5..f80dca3223 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -8,33 +8,9 @@
 
 (*i $Id$ i*)
 
+open Cdglobals
 open Index
 
-type target_language = LaTeX | HTML | TeXmacs
-
-val target_language : target_language ref
-
-val set_out_file : string -> unit
-val output_dir : string ref
-val close : unit -> unit
-
-val quiet : bool ref
-val short : bool ref
-val light : bool ref
-val header_trailer : bool ref
-val index : bool ref
-val multi_index : bool ref
-val toc : bool ref
-val title : string ref
-val externals : bool ref
-val coqlib : string ref
-val raw_comments : bool ref
-
-val charset : string ref
-val inputenc : string ref
-val set_latin1 : unit -> unit
-val set_utf8 : unit -> unit
-
 val add_printing_token : string -> string option * string option -> unit
 val remove_printing_token : string -> unit
 
@@ -45,8 +21,6 @@ val trailer : unit -> unit
 
 val push_in_preamble : string -> unit
 
-val dump_file : string -> unit
-
 val start_module : unit -> unit
 
 val start_doc : unit -> unit
diff --git a/tools/coqdoc/pretty.mli b/tools/coqdoc/pretty.mli
index e7314a1b53..f02a79be50 100644
--- a/tools/coqdoc/pretty.mli
+++ b/tools/coqdoc/pretty.mli
@@ -10,10 +10,4 @@
 
 open Index
 
-type file =
-  | Vernac_file of string * coq_module
-  | Latex_file of string
-
-val gallina : bool ref
-
-val produce_document : file list -> unit
+val coq_file : string -> Cdglobals.coq_module -> unit
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 29119e3f86..9d695950cd 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -12,6 +12,7 @@
 
 {
 
+  open Cdglobals
   open Printf
   open Index
   open Lexing 
@@ -56,44 +57,8 @@
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
 
-  (* Gallina (skipping proofs). This is a three states automaton. *)   
-
-  let gallina = ref false
-
-  type gallina_state = Nothing | AfterDot | Proof
-
-  let gstate = ref AfterDot
-
-  let glet = ref false
-
-  let is_proof = 
-    let t = Hashtbl.create 13 in
-    List.iter (fun s -> Hashtbl.add t s true)
-      [ "Theorem"; "Lemma"; "Fact"; "Remark"; "Goal"; "Let";
-	"Correctness"; "Definition"; "Morphism" ];
-    fun s -> try Hashtbl.find t s with Not_found -> false
-
-  let gallina_id id = 
-    if !gstate = AfterDot then
-      if is_proof id then gstate := Proof else 
-	if id <> "Add" then gstate := Nothing
-
-  let gallina_symbol s = 
-    if !gstate = AfterDot then 
-      gstate := Nothing
-    else
-      if (!gstate = Proof && s = ":=") then 
-	if !glet then glet := false else gstate := Nothing
-
   let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
 
-  let gallina_char c = 
-    if c = '.' then
-      (let skip = !gstate = Proof in gstate := AfterDot; skip)
-    else
-      (if !gstate = AfterDot && not (is_space c) then gstate := Nothing;
-       false)
-
   (* saving/restoring the PP state *)
 
   type state = {
@@ -126,9 +91,7 @@
 
   let reset () =
     formatted := false;
-    brackets := 0;
-    gstate := AfterDot;
-    glet := false
+    brackets := 0
 
   (* erasing of Section/End *)
 
@@ -222,6 +185,100 @@ let symbolchar_no_brackets =
 let symbolchar = symbolchar_no_brackets | '[' | ']'
 let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
 
+
+let thm_token = 
+  "Theorem" 
+  | "Lemma" 
+  | "Fact" 
+  | "Remark" 
+  | "Corollary" 
+  | "Proposition" 
+  | "Property"
+  | "Goal"
+
+let def_token = 
+  "Definition" 
+  | "Let" 
+  | "SubClass" 
+  | "Example"
+  | "Local" 
+  | "Fixpoint" 
+  | "CoFixpoint" 
+  | "Record" 
+  | "Structure" 
+  | "Scheme"
+  | "Inductive"
+  | "CoInductive"
+
+let decl_token = 
+  "Hypothesis" 
+  | "Hypotheses" 
+  | "Parameter" 
+  | "Axiom" 's'? 
+  | "Conjecture"
+
+let gallina_ext =
+  "Module" 
+  | "Declare"
+  | "Transparent"
+  | "Opaque"
+  | "Canonical"
+  | "Coercion"
+  | "Identity"
+  | "Implicit"
+  | "Notation"
+  | "Infix"
+  | "Tactic" space+ "Notation"
+  | "Reserved" space+ "Notation"
+
+let commands = 
+  "Pwd"
+  | "Cd"
+  | "Drop"
+  | "ProtectedLoop"
+  | "Quit"
+  | "Load"
+  | "Add"
+  | "Remove" space+ "Loadpath"
+  | "Print"
+  | "Inspect"
+  | "About"
+  | "Search"
+  | "Eval"
+  | "Reset"
+  | "Check"
+  | "Type"
+
+let extraction = 
+  "Extraction"
+  | "Recursive" space+ "Extraction" 
+  | "Extract"
+
+let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
+
+let gallina_kw_to_hide =
+  "Implicit"
+  | "Ltac"
+  | "Require"
+  | "Import"
+  | "Export"
+  | "Load" 
+  | "Hint"
+  | "Open"
+  | "Close"
+  | "Delimit"
+  | "Transparent"
+  | "Opaque"
+  | ("Declare" space+ ("Morphism" | "Step") )
+  | "Section"
+  | "Chapter"
+  | "Variable" 's'?
+  | ("Hypothesis" | "Hypotheses")
+  | "End"
+  | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
+  | "Declare" space+ ("Left" | "Right") space+ "Step" 
+
+
 (* tokens with balanced brackets *)
 let token_brackets =
   ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* 
@@ -241,21 +298,7 @@ let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
 let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 *)
 
-let coq_command_to_hide =
-  "Implicit" space |
-  "Ltac" space | 
-  "Require" space | 
-  "Load" space |
-  "Hint" space |
-  "Transparent" space |
-  "Opaque" space |
-  ("Declare" space+ ("Morphism" | "Step") space) |
-  "Section" space | 
-  "Variable" 's'? space | 
-  ("Hypothesis" | "Hypotheses") space | 
-  "End" space |
-  ("Set" | "Unset") space+ "Printing" space+ "Coercions" space |
-  "Declare" space+ ("Left" | "Right") space+ "Step" space
+
 
 (*s Scanning Coq, at beginning of line *)
 
@@ -265,8 +308,8 @@ rule coq_bol = parse
   | space* "(**" space_nl
       { end_coq (); start_doc (); 
 	let eol = doc_bol lexbuf in
-	end_doc (); start_coq (); 
-	if eol then coq_bol lexbuf else coq lexbuf }
+	  end_doc (); start_coq (); 
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | space* "Comments" space_nl
       { end_coq (); start_doc (); comments lexbuf; end_doc (); 
 	start_coq (); coq lexbuf }
@@ -276,28 +319,35 @@ rule coq_bol = parse
       { begin_show (); coq_bol lexbuf }
   | space* end_show
       { end_show (); coq_bol lexbuf }
-  | space* coq_command_to_hide
+  | space* gallina_kw_to_hide
       { let s = lexeme lexbuf in
-	if !light && section_or_end s then begin 
-	  skip_to_dot lexbuf; 
-	  coq_bol lexbuf 
-	end else begin
-	  indentation (count_spaces s); 
-	  backtrack lexbuf; 
-	  coq lexbuf 
-	end }
+	  if !light && section_or_end s then begin 
+	    skip_to_dot lexbuf; 
+	    coq_bol lexbuf 
+	  end else begin
+	    indentation (count_spaces s); 
+	    ident s (lexeme_start lexbuf); 
+	    let eol= body lexbuf in 
+	      if eol then coq_bol lexbuf else coq lexbuf
+	  end }
+  | space* gallina_kw
+      { let s = lexeme lexbuf in 
+	  indentation (count_spaces s);
+	  ident s (lexeme_start lexbuf); 
+	  let eol= body lexbuf in
+	    if eol then coq_bol lexbuf else coq lexbuf }
   | space* "(**" space+ "printing" space+ (identifier | token) space+
       { let tok = lexeme lexbuf in
 	let s = printing_token lexbuf in
-	add_printing_token tok s;
-	coq_bol lexbuf }
+	  add_printing_token tok s;
+	  coq_bol lexbuf }
   | space* "(**" space+ "printing" space+
       { eprintf "warning: bad 'printing' command at character %d\n" 
 	  (lexeme_start lexbuf); flush stderr;
 	ignore (comment lexbuf);
 	coq_bol lexbuf }
   | space* "(**" space+ "remove" space+ "printing" space+ 
-    (identifier | token) space* "*)"
+      (identifier | token) space* "*)"
       { remove_printing_token (lexeme lexbuf);
 	coq_bol lexbuf }
   | space* "(**" space+ "remove" space+ "printing" space+
@@ -307,24 +357,28 @@ rule coq_bol = parse
 	coq_bol lexbuf }
   | space* "(*"
       { let eol = comment lexbuf in
-	if eol then coq_bol lexbuf else coq lexbuf }
-  | space+
-      { indentation (count_spaces (lexeme lexbuf)); coq lexbuf }
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | eof 
       { () }
-  | _ 
-      { backtrack lexbuf; indentation 0; coq lexbuf }
+  | _
+      { let eol = 
+	  if not !gallina then 
+	    begin backtrack lexbuf; indentation 0; body_bol lexbuf end 
+	  else 
+	    skip_to_dot lexbuf 
+	in
+	  if eol then coq_bol lexbuf else coq lexbuf }
 
 (*s Scanning Coq elsewhere *)
 
 and coq = parse
   | "\n" 
-      { line_break (); coq_bol lexbuf }
+      { line_break(); coq_bol lexbuf }
   | "(**" space_nl
       { end_coq (); start_doc (); 
 	let eol = doc_bol lexbuf in
-	end_doc (); start_coq (); 
-	if eol then coq_bol lexbuf else coq lexbuf }
+	  end_doc (); start_coq (); 
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | "(*"
       { let eol = comment lexbuf in
 	  if eol then begin line_break(); coq_bol lexbuf end 
@@ -334,45 +388,44 @@ and coq = parse
       { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end }
   | eof 
       { () }
-  | "let" { let s = lexeme lexbuf in
-	      glet:=true; ident s (lexeme_start lexbuf); coq lexbuf }
-  | token
+  | gallina_kw_to_hide
       { let s = lexeme lexbuf in
-	if !gallina then gallina_symbol s;
-	symbol s;
-	coq lexbuf }
-  | "with" space+ "Module" | "Module" space+ "Type" | "Declare" space+ "Module"
-    (* hack to avoid making Type a keyword *)
-      { let s = lexeme lexbuf in
-	if !gallina then gallina_id s;
-        ident s (lexeme_start lexbuf); coq lexbuf }
-  | "(" space* identifier space* ":=" 
-      { let id = extract_ident (lexeme lexbuf) in
-	symbol "("; ident id (lexeme_start lexbuf); symbol ":="; coq lexbuf }
-  | (identifier '.')* identifier
-      { let id = lexeme lexbuf in
-	if !gallina then gallina_id id;
-	ident id (lexeme_start lexbuf); coq lexbuf }
-  | _ 
-      { let c = lexeme_char lexbuf 0 in 
-	char c;
-	if !gallina && gallina_char c then skip_proof lexbuf;
-	coq lexbuf }
-
+	  if !light && section_or_end s then begin 
+	    let eol = skip_to_dot lexbuf in
+	      if eol then coq_bol lexbuf else coq lexbuf 
+	  end else begin
+	    ident s (lexeme_start lexbuf); 
+	    let eol=body lexbuf in 
+	      if eol then coq_bol lexbuf else coq lexbuf
+	  end }
+  | gallina_kw
+      { let s = lexeme lexbuf in 
+	  ident s (lexeme_start lexbuf); 
+	  let eol = body lexbuf in
+	    if eol then coq_bol lexbuf else coq lexbuf }
+  | space+ { char ' '; coq lexbuf }
+  | _ { let eol = 
+	  if not !gallina then 
+	    begin backtrack lexbuf; indentation 0; body_bol lexbuf end 
+	  else 
+	    skip_to_dot lexbuf 
+	in 
+	  if eol then coq_bol lexbuf else coq lexbuf}
+      
 (*s Scanning documentation, at beginning of line *)
-
+      
 and doc_bol = parse
   | space* "\n" '\n'*
       { paragraph (); doc_bol lexbuf }
   | space* section [^')'] ([^'\n' '*'] | '*' [^'\n'')'])*
-      { let lev, s = sec_title (lexeme lexbuf) in 
-	section lev (fun () -> ignore (doc (from_string s))); 
-	doc lexbuf }
-  | space* '-'+
-      { let n = count_dashes (lexeme lexbuf) in
-	if n >= 4 then rule () else item n;
-	doc lexbuf }
-  | "<<" space*
+{ let lev, s = sec_title (lexeme lexbuf) in 
+    section lev (fun () -> ignore (doc (from_string s))); 
+    doc lexbuf }
+| space* '-'+
+     { let n = count_dashes (lexeme lexbuf) in
+	 if n >= 4 then rule () else item n;
+	 doc lexbuf }
+| "<<" space*
       { start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
   | eof 
       { false }
@@ -491,23 +544,30 @@ and comment = parse
   | eof  { false }
   | _    { comment lexbuf }
 
-(*s Skip proofs *)
-
-and skip_proof = parse
-  | "(*" { ignore (comment lexbuf); skip_proof lexbuf }
-  | "Save" | "Qed" | "Defined"
-  | "Abort" | "Proof" | "Admitted" { skip_to_dot lexbuf }
-  | "Proof" space* '.' { skip_proof lexbuf }
-  | identifier { skip_proof lexbuf } (* to avoid keywords within idents *)
-  | eof { () }
-  | _ { skip_proof lexbuf }
-
 and skip_to_dot = parse
-  | eof | '.' space { if !gallina then gstate := AfterDot }
-  | ".\n" { if !gallina then gstate := AfterDot; line_break(); }
+  | '.' space* '\n' { true }
+  | eof | '.' space+ { false}
   | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
   | _ { skip_to_dot lexbuf }
 
+and body_bol = parse
+  | space+
+      { indentation (count_spaces (lexeme lexbuf)); body lexbuf }
+  | _ { backtrack lexbuf; body lexbuf }
+
+and body = parse
+  | '\n' {line_break(); body_bol lexbuf}
+  | eof { false }
+  | '.' space* '\n' { char '.'; line_break(); true }      
+  | '.' space+ { char '.'; char ' '; false }
+  | "(*" { let eol = comment lexbuf in 
+	     if eol then body_bol lexbuf else body lexbuf }
+  | identifier 
+      { let s = lexeme lexbuf in 
+	  ident s (lexeme_start lexbuf); body lexbuf }
+  | _ { let c = lexeme_char lexbuf 0 in 
+	  char c; body lexbuf }
+
 and skip_hide = parse
   | eof | end_hide { () }
   | _ { skip_hide lexbuf }
@@ -526,10 +586,6 @@ and printing_token = parse
 
 {
 
-  type file =
-    | Vernac_file of string * coq_module
-    | Latex_file of string
-
   let coq_file f m =
     reset ();
     Index.scan_file f m;
@@ -539,59 +595,5 @@ and printing_token = parse
     start_coq (); coq_bol lb; end_coq ();
     close_in c
 
-  (* LaTeX document *)
-
-  let latex_document l = 
-    let file = function
-      | Vernac_file (f,m) -> set_module m; coq_file f m
-      | Latex_file f -> dump_file f
-    in
-    header ();
-    if !toc then make_toc ();
-    List.iter file l;
-    trailer ();
-    close ()
-
-  (* HTML document *)      
-
-  let html_document l =
-    let file = function
-      | Vernac_file (f,m) -> 
-	  set_module m;
-	  let hf = m ^ ".html" in
-	  set_out_file hf;
-	  header ();
-	  coq_file f m;
-	  trailer ();
-	  close ()
-      | Latex_file _ -> ()
-    in
-    List.iter file l;
-    make_index ();
-    if !toc then make_toc ()
-
-  (* TeXmacs document *)
-
-  let texmacs_document l = 
-    let file = function
-      | Vernac_file (f,m) -> set_module m; coq_file f m
-      | Latex_file f -> dump_file f
-    in
-    header ();
-    List.iter file l;
-    trailer ();
-    close ()
-
-  let index_module = function
-    | Vernac_file (_,m) -> Index.add_module m
-    | Latex_file _ -> ()
-
-  let produce_document l =
-    List.iter index_module l;
-    (match !target_language with
-       | LaTeX -> latex_document 
-       | HTML -> html_document
-       | TeXmacs -> texmacs_document) l
-
 }