traducteur: affiche les commentaires a l'interieur des commandes

extraction: pb avec les variables de section definies


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

18 files changed, 496 insertions, 293 deletions

diff --git a/.depend b/.depend
index 7fa1643781..bc5b9bcc51 100644
--- a/.depend
+++ b/.depend
@@ -45,10 +45,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/univ.cmi 
 kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
-kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi 
 kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi 
+kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi 
 kernel/names.cmi: lib/pp.cmi lib/predicate.cmi 
 kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
@@ -68,9 +68,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/bignat.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 
 library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \
     kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \
@@ -99,6 +96,9 @@ library/library.cmi: library/libnames.cmi library/libobject.cmi \
 library/nameops.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
     lib/util.cmi 
+lib/rtree.cmi: lib/pp.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \
     library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \
     lib/util.cmi 
@@ -318,11 +318,11 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
-toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
     library/libnames.cmi kernel/names.cmi kernel/term.cmi \
     interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
+toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \
     parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
     kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
@@ -340,11 +340,11 @@ contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi
 contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi 
 contrib/correctness/past.cmi: kernel/names.cmi contrib/correctness/ptype.cmi \
     kernel/term.cmi interp/topconstr.cmi lib/util.cmi 
-contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
-    pretyping/rawterm.cmi 
 contrib/correctness/pcicenv.cmi: kernel/names.cmi \
     contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
     kernel/sign.cmi kernel/term.cmi 
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+    pretyping/rawterm.cmi 
 contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
     contrib/correctness/ptype.cmi 
 contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi 
@@ -493,6 +493,14 @@ ide/config_lexer.cmo: ide/config_parser.cmi lib/util.cmi
 ide/config_lexer.cmx: ide/config_parser.cmx lib/util.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: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
+    ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
+    ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi ide/undo.cmi \
+    lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi 
+ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
+    ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
+    ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx ide/undo.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi 
 ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
     kernel/declarations.cmi kernel/environ.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \
@@ -515,14 +523,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
     toplevel/vernacentries.cmx toplevel/vernacexpr.cmx ide/coq.cmi 
 ide/coq_tactics.cmo: ide/coq_tactics.cmi 
 ide/coq_tactics.cmx: ide/coq_tactics.cmi 
-ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
-    ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
-    ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi ide/undo.cmi \
-    lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi 
-ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
-    ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
-    ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx ide/undo.cmx \
-    lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi 
 ide/find_phrase.cmo: ide/ideutils.cmi 
 ide/find_phrase.cmx: ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmi 
@@ -671,6 +671,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
 kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
     kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi 
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+    kernel/univ.cmi lib/util.cmi kernel/modops.cmi 
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+    kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+    kernel/univ.cmx lib/util.cmx kernel/modops.cmi 
 kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -679,12 +685,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
     kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
     kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
     kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi 
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
-    kernel/univ.cmi lib/util.cmi kernel/modops.cmi 
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
-    kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
-    kernel/univ.cmx lib/util.cmx kernel/modops.cmi 
 kernel/names.cmo: lib/hashcons.cmi lib/options.cmi lib/pp.cmi \
     lib/predicate.cmi lib/util.cmi kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/options.cmx lib/pp.cmx \
@@ -765,10 +765,10 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
 lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.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/gmap.cmi lib/util.cmi lib/gmapl.cmi 
 lib/gmapl.cmx: lib/gmap.cmx lib/util.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 
@@ -777,24 +777,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/pp.cmi lib/util.cmi lib/rtree.cmi 
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/util.cmi 
 library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \
     library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \
     library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
@@ -852,12 +842,12 @@ library/goptions.cmx: library/lib.cmx library/libnames.cmx \
 library/impargs.cmo: kernel/declarations.cmi kernel/environ.cmi \
     library/global.cmi kernel/inductive.cmi library/lib.cmi \
     library/libnames.cmi library/libobject.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi kernel/reduction.cmi \
+    library/nametab.cmi lib/options.cmi lib/pp.cmi kernel/reduction.cmi \
     library/summary.cmi kernel/term.cmi lib/util.cmi library/impargs.cmi 
 library/impargs.cmx: kernel/declarations.cmx kernel/environ.cmx \
     library/global.cmx kernel/inductive.cmx library/lib.cmx \
     library/libnames.cmx library/libobject.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx kernel/reduction.cmx \
+    library/nametab.cmx lib/options.cmx lib/pp.cmx kernel/reduction.cmx \
     library/summary.cmx kernel/term.cmx lib/util.cmx library/impargs.cmi 
 library/lib.cmo: library/libnames.cmi library/libobject.cmi \
     library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
@@ -899,6 +889,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
     lib/system.cmx library/states.cmi 
 library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi 
+lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/util.cmi 
 parsing/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \
     parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
     toplevel/vernacexpr.cmo 
@@ -1097,8 +1097,8 @@ parsing/g_zsyntax.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmx \
     lib/pp.cmx pretyping/rawterm.cmx interp/symbols.cmx parsing/termast.cmx \
     interp/topconstr.cmx lib/util.cmx parsing/g_zsyntax.cmi 
-parsing/lexer.cmo: lib/pp.cmi parsing/lexer.cmi 
-parsing/lexer.cmx: lib/pp.cmx parsing/lexer.cmi 
+parsing/lexer.cmo: lib/options.cmi lib/pp.cmi parsing/lexer.cmi 
+parsing/lexer.cmx: lib/options.cmx lib/pp.cmx parsing/lexer.cmi 
 parsing/pcoq.cmo: parsing/ast.cmi parsing/coqast.cmi library/decl_kinds.cmo \
     parsing/extend.cmi interp/genarg.cmi parsing/lexer.cmi \
     library/libnames.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
@@ -1949,18 +1949,18 @@ tactics/tactics.cmx: proofs/clenv.cmx interp/constrintern.cmx \
     pretyping/termops.cmx lib/util.cmx tactics/tactics.cmi 
 tactics/tauto.cmo: parsing/ast.cmi toplevel/cerrors.cmi parsing/coqast.cmi \
     parsing/egrammar.cmi interp/genarg.cmi tactics/hipattern.cmi \
-    library/libnames.cmi kernel/names.cmi lib/options.cmi \
-    pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
-    proofs/proof_type.cmi pretyping/rawterm.cmi proofs/refiner.cmi \
-    proofs/tacexpr.cmo tactics/tacinterp.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi interp/topconstr.cmi lib/util.cmi 
+    library/libnames.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
+    lib/pp.cmi parsing/pptactic.cmi proofs/proof_type.cmi \
+    pretyping/rawterm.cmi proofs/refiner.cmi proofs/tacexpr.cmo \
+    tactics/tacinterp.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    interp/topconstr.cmi lib/util.cmi 
 tactics/tauto.cmx: parsing/ast.cmx toplevel/cerrors.cmx parsing/coqast.cmx \
     parsing/egrammar.cmx interp/genarg.cmx tactics/hipattern.cmx \
-    library/libnames.cmx kernel/names.cmx lib/options.cmx \
-    pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
-    proofs/proof_type.cmx pretyping/rawterm.cmx proofs/refiner.cmx \
-    proofs/tacexpr.cmx tactics/tacinterp.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx interp/topconstr.cmx lib/util.cmx 
+    library/libnames.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
+    lib/pp.cmx parsing/pptactic.cmx proofs/proof_type.cmx \
+    pretyping/rawterm.cmx proofs/refiner.cmx proofs/tacexpr.cmx \
+    tactics/tacinterp.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    interp/topconstr.cmx lib/util.cmx 
 tactics/termdn.cmo: tactics/dn.cmi library/libnames.cmi library/nameops.cmi \
     kernel/names.cmi library/nametab.cmi pretyping/pattern.cmi \
     pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi tactics/termdn.cmi 
@@ -1979,10 +1979,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
     pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
     tactics/wcclausenv.cmi 
-tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
-tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
 tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
 tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
+tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
 tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
@@ -2191,18 +2191,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \
     toplevel/vernac.cmx toplevel/vernacexpr.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: interp/constrextern.cmi interp/constrintern.cmi \
-    parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
-    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
-    lib/pp.cmi translate/ppvernacnew.cmi library/states.cmi lib/system.cmi \
-    lib/util.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
-    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
-    parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
-    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
-    lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx lib/system.cmx \
-    lib/util.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
-    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
     pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
     interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
@@ -2263,6 +2251,18 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
     kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \
     proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi 
+toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \
+    parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
+    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmi translate/ppvernacnew.cmi library/states.cmi lib/system.cmi \
+    lib/util.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
+    parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
+    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+    lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx lib/system.cmx \
+    lib/util.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \
     interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \
     pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -2341,6 +2341,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
     lib/pp.cmx parsing/pptactic.cmx proofs/proof_type.cmx proofs/refiner.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \
     pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \
@@ -2357,18 +2369,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \
     kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
     interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi 
-contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
-    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
-    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
-    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
-    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pdb.cmo: library/global.cmi kernel/names.cmi \
     library/nametab.cmi contrib/correctness/past.cmi \
     contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -3047,6 +3047,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \
     contrib/interface/pbp.cmi 
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+    parsing/printer.cmi contrib/interface/translate.cmi \
+    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+    parsing/printer.cmx contrib/interface/translate.cmx \
+    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \
     parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \
     pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -3071,14 +3079,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.cmx \
     pretyping/termops.cmx contrib/interface/translate.cmx \
     pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/interface/showproof.cmi 
-contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
-    parsing/printer.cmi contrib/interface/translate.cmi \
-    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
-    parsing/printer.cmx contrib/interface/translate.cmx \
-    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     interp/constrextern.cmi contrib/interface/ctast.cmo kernel/environ.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi library/libobject.cmi \
@@ -3309,12 +3309,12 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
     proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx lib/util.cmx 
-contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi 
-contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx 
 contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \
     kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi 
 contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \
     kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx 
+contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi 
+contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx 
 contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo library/declare.cmi \
     library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \
     kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
@@ -3369,8 +3369,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \
     contrib/xml/xml.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/acic.cmo contrib/xml/acic2Xml.cmo \
     contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
@@ -3395,10 +3393,8 @@ contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
 contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
     lib/util.cmx toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx 
-ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
-    ide/utils/configwin_types.cmo ide/utils/configwin.cmi 
-ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
-    ide/utils/configwin_types.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/configwin_ihm.cmo \
     ide/utils/configwin_messages.cmo ide/utils/configwin_types.cmo \
     ide/utils/uoptions.cmi 
@@ -3409,6 +3405,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/configwin_messages.cmo \
     ide/utils/configwin_types.cmo ide/utils/okey.cmi ide/utils/uoptions.cmi 
 ide/utils/configwin_ihm.cmx: ide/utils/configwin_messages.cmx \
     ide/utils/configwin_types.cmx ide/utils/okey.cmx ide/utils/uoptions.cmx 
+ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
+    ide/utils/configwin_types.cmo ide/utils/configwin.cmi 
+ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
+    ide/utils/configwin_types.cmx ide/utils/configwin.cmi 
 ide/utils/configwin_types.cmo: ide/utils/configwin_keys.cmo \
     ide/utils/uoptions.cmi 
 ide/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index a4c2cc46e3..df1069c184 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -352,10 +352,11 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	let n = nb_default_params env mip0.mind_nf_arity in
 	let projs = try List.map out_some projs with _ -> raise (I Standard) in
 	let is_true_proj kn = 
-	  match kind_of_term (snd (decompose_lam (constant_value env kn))) with 
-	    | Rel _ -> false 
-	    | Case _ -> true
-	    | _ -> assert false
+          let (_,body) = Sign.decompose_lam_assum (constant_value env kn) in
+          match kind_of_term body with
+              | Rel _ -> false
+              | Case _ -> true
+              | _ -> assert false
 	in 
 	let projs = List.filter is_true_proj projs in 
  	let rec check = function 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e915c9ac62..b34ae524f2 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -548,17 +548,17 @@ let rec extern inctx scopes vars r =
 	  (f,args) in
       (match f with
 	 | REvar (loc,ev) -> extern_evar loc ev (* we drop args *)
-	 | RRef (loc,ref) ->
+	 | RRef (rloc,ref) ->
 	     let subscopes = Symbols.find_arguments_scope ref in
 	     let args =
 	       extern_args (extern true) (snd scopes) vars args subscopes in
 	     extern_app loc inctx (implicits_of_global_out ref)
-               (Some ref,extern_reference loc vars ref)
+               (Some ref,extern_reference rloc vars ref)
 	       args
-	 | RVar (loc,id) -> (* useful for translation of inductive *)
+	 | RVar (rloc,id) -> (* useful for translation of inductive *)
 	     let args = List.map (sub_extern true scopes vars) args in
 	     extern_app loc inctx (get_temporary_implicits_out id)
-	       (None,Ident (loc,v7_to_v8_id id))
+	       (None,Ident (rloc,v7_to_v8_id id))
 	       args
 	 | _       -> 
 	     explicitize loc inctx [] (None,sub_extern false scopes vars f)
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 14726f8aa8..7e18dcf806 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -22,7 +22,18 @@ open Pp_control
       (except if no mark yet on the reste of the line)
    \end{description}
  *)
-   
+ 
+let comments = ref []
+  
+let rec split_com comacc acc pos = function
+    [] -> comments := List.rev acc; comacc
+  | ((b,e),c as com)::coms ->
+      (* Take all comments that terminates before pos, or begin exactly
+         at pos (used to print comments attached after an expression) *)
+      if e<=pos || pos=b then split_com (c::comacc) acc pos coms
+      else  split_com comacc (com::acc) pos coms
+
+
 type block_type =
   | Pp_hbox of int
   | Pp_vbox of int
@@ -42,6 +53,7 @@ type 'a ppcmd_token =
   | Ppcmd_open_box of block_type
   | Ppcmd_close_box
   | Ppcmd_close_tbox
+  | Ppcmd_comment of int
 
 type 'a ppdir_token =
   | Ppdir_ppcmds of 'a ppcmd_token Stream.t
@@ -99,6 +111,7 @@ let tab () = [< 'Ppcmd_set_tab >]
 let fnl () = [< 'Ppcmd_force_newline >]
 let pifb () = [< 'Ppcmd_print_if_broken >]
 let ws n = [< 'Ppcmd_white_space n >]
+let comment n = [< ' Ppcmd_comment n >]
 
 (* derived commands *)
 let mt () = [< >]
@@ -118,6 +131,7 @@ let rec escape_string s =
     else escape_at s (i-1) in
   escape_at s (String.length s - 1)
 
+
 let qstring s = str ("\""^(escape_string s)^"\"")
 let qs = qstring
 
@@ -139,6 +153,34 @@ let tclose () = [< 'Ppcmd_close_tbox >]
 
 let (++) = Stream.iapp
 
+(* This flag tells if the last printed comment ends with a newline, to
+  avoid empty lines *)
+let com_eol = ref false
+
+let com_brk ft = com_eol := false
+let com_if ft f =
+  if !com_eol then (com_eol := false; Format.pp_force_newline ft ())
+  else Lazy.force f
+
+let rec pr_com ft s =
+  let (s1,os) =
+    try
+      let n = String.index s '\n' in
+      String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1))
+    with Not_found -> s,None in
+  com_if ft (Lazy.lazy_from_val());
+(*  let s1 =
+    if String.length s1 <> 0 && s1.[0] = ' ' then
+      (Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1))
+    else s1 in*)
+  Format.pp_print_as ft (utf8_length s1) s1;
+  match os with
+      Some s2 ->
+        if String.length s2 = 0 then (com_eol := true)
+        else
+          (Format.pp_force_newline ft (); pr_com ft s2)
+    | None -> ()
+
 (* pretty printing functions *)
 let pp_dirs ft = 
   let maxbox = (get_gp ft).max_depth in
@@ -150,29 +192,42 @@ let pp_dirs ft =
     | Pp_tbox     -> Format.pp_open_tbox ft () 
   in
   let rec pp_cmd = function
-    | Ppcmd_print(n,s)        -> Format.pp_print_as ft n s
+    | Ppcmd_print(n,s)        ->
+        com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s
     | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
+        com_if ft (Lazy.lazy_from_val());
         pp_open_box bty ;
         if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss;
         Format.pp_close_box ft ()
-    | Ppcmd_open_box bty      -> pp_open_box bty
+    | Ppcmd_open_box bty      -> com_if ft (Lazy.lazy_from_val()); pp_open_box bty
     | Ppcmd_close_box         -> Format.pp_close_box ft ()
     | Ppcmd_close_tbox        -> Format.pp_close_tbox ft ()
-    | Ppcmd_white_space n     -> Format.pp_print_break ft n 0
-    | Ppcmd_print_break(m,n)  -> Format.pp_print_break ft m n
+    | Ppcmd_white_space n     ->
+        com_if ft (Lazy.lazy_from_fun (fun()->Format.pp_print_break ft n 0))
+    | Ppcmd_print_break(m,n)  ->
+        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_break ft m n))
     | Ppcmd_set_tab           -> Format.pp_set_tab ft ()
-    | Ppcmd_print_tbreak(m,n) -> Format.pp_print_tbreak ft m n
-    | Ppcmd_force_newline     -> Format.pp_force_newline ft ()
-    | Ppcmd_print_if_broken   -> Format.pp_print_if_newline ft () 
+    | Ppcmd_print_tbreak(m,n) ->
+        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_tbreak ft m n))
+    | Ppcmd_force_newline     ->
+        com_brk ft; Format.pp_force_newline ft ()
+    | Ppcmd_print_if_broken   ->
+        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_if_newline ft ()))
+    | Ppcmd_comment i         ->
+        let coms = split_com [] [] i !comments in
+(*        Format.pp_open_hvbox ft 0;*)
+        List.iter (pr_com ft) coms(*;
+        Format.pp_close_box ft ()*)
   in
   let pp_dir = function
     | Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream
-    | Ppdir_print_newline    -> Format.pp_print_newline ft ()
+    | Ppdir_print_newline    ->
+        com_brk ft; Format.pp_print_newline ft ()
     | Ppdir_print_flush      -> Format.pp_print_flush ft () 
   in
   fun dirstream ->
     try  
-      Stream.iter pp_dir dirstream
+      Stream.iter pp_dir dirstream; com_brk ft
     with 
       | e -> Format.pp_print_flush ft () ; raise e
 
diff --git a/lib/pp.mli b/lib/pp.mli
index c23100b2f8..0af314f17d 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -30,6 +30,9 @@ val pifb : unit -> std_ppcmds
 val ws : int -> std_ppcmds
 val mt : unit -> std_ppcmds
 
+val comment : int -> std_ppcmds
+val comments : ((int * int) * string) list ref
+
 (*s Concatenation. *)
 
 val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 43879c3b63..cde0a59b55 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -44,6 +44,31 @@ let coerce_to_name = function
         (constr_loc ast,"Ast.coerce_to_var",
          (Pp.str"This expression should be a simple identifier"))
 
+let set_loc loc = function
+  | CRef(Ident(_,i)) -> CRef(Ident(loc,i))
+  | CRef(Qualid(_,q)) -> CRef(Qualid(loc,q))
+  | CFix(_,x,a) -> CFix(loc,x,a)
+  | CCoFix(_,x,a) -> CCoFix(loc,x,a)
+  | CArrow(_,a,b) -> CArrow(loc,a,b)
+  | CProdN(_,bl,a) -> CProdN(loc,bl,a)
+  | CLambdaN(_,bl,a) -> CLambdaN(loc,bl,a)
+  | CLetIn(_,x,a,b) -> CLetIn(loc,x,a,b)
+  | CAppExpl(_,f,a) -> CAppExpl(loc,f,a)
+  | CApp(_,f,a) -> CApp(loc,f,a)
+  | CCases(_,p,a,br) -> CCases(loc,p,a,br)
+  | COrderedCase(_,s,p,a,br) -> COrderedCase(loc,s,p,a,br)
+  | CLetTuple(_,ids,p,a,b) -> CLetTuple(loc,ids,p,a,b)
+  | CIf(_,e,p,a,b) -> CIf(loc,e,p,a,b)
+  | CHole _ -> CHole loc
+  | CPatVar(_,v) -> CPatVar(loc,v)
+  | CEvar(_,ev) -> CEvar(loc,ev)
+  | CSort(_,s) -> CSort(loc,s)
+  | CCast(_,a,b) -> CCast(loc,a,b)
+  | CNotation(_,n,l) -> CNotation(loc,n,l)
+  | CNumeral(_,i) -> CNumeral(loc,i)
+  | CDelimiters(_,s,e) -> CDelimiters(loc,s,e)
+  | CDynamic(_,d) -> CDynamic(loc,d)
+
 open Util
 
 let rec abstract_constr loc c = function
@@ -195,7 +220,8 @@ GEXTEND Gram
           let id1 = coerce_to_name lc1 in
           let id2 = coerce_to_name lc2 in
 	  CProdN (loc, (id1::id2::idl, c)::bl, body)
-      | "("; lc1 = lconstr; ")" -> lc1
+      | "("; lc1 = lconstr; ")" ->
+          if Options.do_translate() then set_loc loc lc1 else lc1
       | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" ->
 	  (match lc1 with
 	    | CPatVar (loc2,(false,n)) -> 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index bda234764f..d52ced8171 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -33,6 +33,9 @@ let thm_token = G_proofs.thm_token
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
 
+let filter_com (b,e) =
+  Pp.comments := List.filter (fun ((b',e'),s) -> b'<b || e'>e) !Pp.comments 
+
 if !Options.v7 then
 GEXTEND Gram
   GLOBAL: vernac gallina_ext;
@@ -49,7 +52,8 @@ GEXTEND Gram
       | "["; l = vernac_list_tail -> VernacList l
 
       (* For translation from V7 to V8 *)
-      | IDENT "V7only"; v = vernac -> VernacV7only v
+      | IDENT "V7only"; v = vernac ->
+          filter_com loc; VernacV7only v
       | IDENT "V8only"; v = vernac -> VernacV8only v
 
 (*
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 5545f00778..843bd068fa 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -195,61 +195,99 @@ let rec number len = parser
 
 let escape len c = store len c
 
-let rec string bp len = parser
+let rec string_v8 bp len = parser
+  | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] ->
+      if esc then string_v8 bp (store len '"') s else len
+  | [< 'c; s >] -> string_v8 bp (store len c) s 
+  | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
+
+let rec string_v7 bp len = parser
   | [< ''"' >] -> len
   | [< ''\\'; c = (parser [< ' ('"' | '\\' as c) >] -> c | [< >] -> '\\'); s >]
-     -> string bp (escape len c) s
+     -> string_v7 bp (escape len c) s
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
-  | [< 'c; s >] -> string bp (store len c) s 
-
-let comments = ref None
-
-type commentar =
-  | InVernac
-  | InVernacEsc of string
-  | BeVernac of string
-  | InComment of string
-
-let current = ref (BeVernac "")
-
-let add_comment () = let reinit () = match ! current with
-  | InVernac -> ()
-  | InVernacEsc s -> current := InVernacEsc ""
-  | BeVernac s -> current := BeVernac ""
-  | InComment s -> current := InComment "" in
-match (!comments,!current) with
-  | None , InVernac -> ()
-  | None , BeVernac s | None , InComment s | None , InVernacEsc s -> reinit (); comments := Some [str s]
-  | Some _ , InVernac -> ()
-  | Some l , BeVernac s | Some l , InComment s | Some l , InVernacEsc s -> reinit (); comments := Some (str s::l)
-
-let add_comment_pp s = match !comments with
-  | None -> comments := Some [s]
-  | Some l -> comments := Some (s::l) 
-
-let add_string s = match !current with
-  | InVernac -> ()
-  | InVernacEsc t -> current := InVernacEsc (t^s)
-  | BeVernac t -> current := BeVernac (t^s)
-  | InComment t -> current := InComment (t^s)
-	
-let rec comment bp = parser
+  | [< 'c; s >] -> string_v7 bp (store len c) s 
+
+let string bp len s =
+  if !Options.v7 then string_v7 bp len s else string_v8 bp len s
+
+(* Utilities for comment translation *)
+let comment_begin = ref None
+let comm_loc bp = if !comment_begin=None then comment_begin := Some bp
+
+let current = ref ""
+let between_com = ref true
+
+type com_state = int option * string * bool
+let restore_com_state (o,s,b) =
+  comment_begin := o; current := s; between_com := b
+let dflt_com = (None,"",true)
+let com_state () =
+  let s = (!comment_begin, !current, !between_com) in
+  restore_com_state dflt_com; s
+
+let real_push_char c = current := !current ^ String.make 1 c
+
+(* Add a char if it is between two commands, if it is a newline or
+   if the last char is not a space itself. *)
+let push_char c =
+  if
+    !between_com || List.mem c ['\n';'\r'] ||
+    (List.mem c [' ';'\t']&&
+     (String.length !current=0 ||
+      not (List.mem !current.[String.length !current - 1]
+        [' ';'\t';'\n';'\r'])))
+  then
+    real_push_char c
+
+let push_string s = current := !current ^ s
+
+let null_comment s =
+  let rec null i =
+    i<0 || (List.mem s.[i] [' ';'\t';'\n';'\r'] && null (i-1)) in
+  null (String.length s - 1)
+
+let comment_stop ep =
+  (if Options.do_translate() && !current <> "" &&
+    (!between_com || not(null_comment !current)) then
+    let bp = match !comment_begin with
+        Some bp -> bp
+      | None ->
+          msgerrnl(str"No begin location for comment '"++str !current++str"' ending at  "++int ep);
+          ep-1 in
+    Pp.comments := ((bp,ep),!current) :: !Pp.comments);
+  current := "";
+  comment_begin := None;
+  between_com := false
+
+(* Does not unescape!!! *)
+let rec comm_string bp = parser
+  | [< ''"' >] -> push_string "\""
+  | [< ''\\'; _ =
+           (parser [< ' ('"' | '\\' as c) >] ->
+             if c='"' then real_push_char c;
+             real_push_char c
+                 | [< >] -> real_push_char '\\'); s >]
+     -> comm_string bp s
+  | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
+  | [< 'c; s >] -> real_push_char c; comm_string bp s 
+
+let rec comment bp = parser bp2
   | [< ''(';
        _ = (parser
-              | [< ''*'; s >] -> add_string "(*"; comment bp s
-              | [< >] -> add_string "(" ); 
+              | [< ''*'; s >] -> push_string "(*"; comment bp s
+              | [< >] -> push_string "(" ); 
        s >] -> comment bp s
   | [< ''*';
        _ = parser
-         | [< '')' >] -> add_string "*)"; add_comment ()
-         | [< s >] -> add_string "*"; comment bp s >] -> ()
-  | [< ''"'; _ = (parser bp [< _ = string bp 0 >] -> ()); s >] ->
+         | [< '')' >] ep -> push_string "*)"
+         | [< s >] -> real_push_char '*'; comment bp s >] -> ()
+  | [< ''"'; s >] ->
+      if Options.do_translate() then (push_string"\"";comm_string bp2 s)
+      else ignore (string bp2 0 s);
       comment bp s
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment
-  | [< '_ as z; s >] -> 
-	(match z with
-	| '\n' -> add_comment (); add_comment_pp (fnl ())
-	| _ -> add_string (String.make 1 z)); comment bp s 
+  | [< '_ as z; s >] ep -> real_push_char z; comment bp s
 
 (* Parse a special token, using the [token_tree] *)
 
@@ -337,57 +375,57 @@ let parse_after_dot bp c strm =
 (* Parse a token in a char stream *)
 
 let rec next_token = parser bp
-  | [< ''\n'; s >] -> (match !current with
-	| BeVernac s -> current := InComment s
-	| InComment _ -> add_comment_pp (fnl ())
-	| _ -> ()); next_token s
-  | [< '' ' | '\t'; s >] -> (match !current with
-	| BeVernac _ |  InComment _ -> add_comment_pp (spc ())
-	| _ -> ()); next_token s
-  | [< ''\r'; s >] -> next_token s
+  | [< '' ' | '\t' | '\n' |'\r' as c; s >] ep ->
+      comm_loc bp; push_char c; next_token s
   | [< ''$'; len = ident (store 0 '$') >] ep -> 
+      comment_stop bp;
       (("METAIDENT", get_buff len), (bp,ep))
   | [< ''.' as c; t = parse_after_dot bp c >] ep ->
-      current:=BeVernac ""; (t, (bp,ep))
+      comment_stop bp;
+      if !Options.v7 & t=("",".") then between_com := true;
+      (t, (bp,ep))
   | [< ' ('_' | 'a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ep ->
-      let id = get_buff len in current:=InVernac; 
+      let id = get_buff len in 
+      comment_stop bp;
       (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
   (* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
   | [< ' ('\206' | '\207' as c1); ' ('\128'..'\191' as c2); 
 	   len = ident (store (store 0 c1) c2) >] ep ->
-      let id = get_buff len in current:=InVernac; 
+      let id = get_buff len in
+      comment_stop bp;
       (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
   (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *)
   | [< ''\226' as c1; t = parse_226_tail (Some !token_tree) >] ep ->
+      comment_stop bp;
       (match t with
 	| TokSymbol (Some t) -> ("", t), (bp, ep)
 	| TokSymbol None -> err (bp, ep) Undefined_token
 	| TokIdent id ->
-	    current:=InVernac; 
 	    (try ("", find_keyword id) with Not_found -> ("IDENT", id)),
 	    (bp, ep))
   (* iso 8859-1 accentuated letters *)
   | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c);
       len = ident (store 0 c) >] ep ->
-      let id = get_buff len in current:=InVernac; 
+      let id = get_buff len in
+      comment_stop bp;
       (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
   | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
+      comment_stop bp;
       (("INT", get_buff len), (bp, ep))
-  | [< ''"'; len = string bp 0 >] ep ->
+  | [< ''\"'; len = string bp 0 >] ep ->
+      comment_stop bp;
       (("STRING", get_buff len), (bp, ep))
   | [< ' ('(' as c);
-       t = parser
-         | [< ''*'; c; s >] -> (match !current with
-				| InVernac -> current := InVernacEsc "(*"
-				| _ -> current := InComment "(*"); 
-	comment bp c; 
-	(match !current with
-	| InVernacEsc _ -> add_comment_pp (fnl ()); current := InVernac
-	| _ -> ()); 
-	next_token s
-         | [< t = process_chars bp c >] -> t >] -> t
-  | [< 'c; t = process_chars bp c >] -> t
-  | [< _ = Stream.empty >] -> (("EOI", ""), (bp, bp + 1))
+      t = parser
+        | [< ''*'; s >] ->
+            comm_loc bp;
+            push_string "(*";
+	    comment bp s; 
+	    next_token s
+        | [< t = process_chars bp c >] -> comment_stop bp; t >] ->
+      t
+  | [< 'c; t = process_chars bp c >] -> comment_stop bp; t
+  | [< _ = Stream.empty >] -> comment_stop bp; (("EOI", ""), (bp, bp + 1))
 
 (* Location table system for creating tables associating a token count
    to its location in a char stream (the source) *)
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index b36f1ec6e1..a32ca355d4 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -40,4 +40,6 @@ val freeze : unit -> frozen_t
 val unfreeze : frozen_t -> unit
 val init : unit -> unit
 
-val comments : (std_ppcmds list option) ref
+type com_state
+val com_state: unit -> com_state
+val restore_com_state: com_state -> unit
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 03b7c06f08..65d0722c3c 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -80,8 +80,8 @@ Notation Snd := (snd ? ?).
 
 Hints Resolve pair inl inr : core v62.
 
-(** Parsing only of things in [Datatypes.v] *)
 V7only[
+(** Parsing only of things in [Datatypes.v] *)
 Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing, A annot).
 Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing, A annot).
 Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing, A annot).
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 21dd4ccec6..e48b150622 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -40,9 +40,9 @@ Notation "'EXT' x : t | p & q" := (ex2 ? [x:t]p [x:t]q)
   V8only "'EXT2' x : t | p & q" (at level 200, x at level 80).
 ].
 
-(** Parsing only of things in [Logic_type.v] *)
 
 V7only[
+(** Parsing only of things in [Logic_type.v] *)
 Notation "< A > x == y"  := (eq A x y)
    (A annot, at level 1, x at level 0, only parsing).
 
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index e5b516090b..41f26ffda9 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -205,8 +205,8 @@ Syntax constr
   | O [ O ]      -> ["(0)"].
 ].
 
-(* For parsing/printing based on scopes *)
 V7only [
+(* For parsing/printing based on scopes *)
 Module nat_scope.
 Infix 4 "+" plus : nat_scope.
 Infix 3 "*" mult : nat_scope.
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c8d69b26b2..58cd8f53b1 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -100,27 +100,57 @@ let parse_phrase (po, verbch) =
 let just_parsing = ref false
 let chan_translate = ref stdout
 
-let pr_comments = function
-  | None -> mt()
-  | Some l -> h 0 (List.fold_left (++) (mt ()) (List.rev l))
+
+let pr_new_syntax loc ocom =
+  let com = match ocom with
+    | Some (VernacV7only _) ->
+        Options.v7_only := true;
+        mt()
+    | Some VernacNop -> mt()
+    | Some com ->
+	let fs = States.freeze () in
+        let com = pr_vernac com in
+        States.unfreeze fs;
+        com
+    | None -> mt() in
+  Format.set_formatter_out_channel !chan_translate;
+  Format.set_max_boxes max_int;
+  if !translate_file then
+    msg (hov 0 (
+(*str"{"++int (fst loc)++str"}"++List.fold_right (fun ((b,e),s) strm -> str"("++int b++str","++int
+  e++str":"++str s++str")"++strm)
+  !Pp.comments (mt()) ++*)
+comment (fst loc) ++ com ++ comment (snd loc - 1)))
+  else
+    msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ com));
+  Constrintern.set_temporary_implicits_in [];
+  Constrextern.set_temporary_implicits_out [];
+  Format.set_formatter_out_channel stdout
 
 let rec vernac_com interpfun (loc,com) =
   let rec interp = function
     | VernacLoad (verbosely, fname) ->
         let ch = !chan_translate in
-        if Options.do_translate () then begin
+        let cs = Lexer.com_state() in
+        let cl = !Pp.comments in
+        if Options.do_translate() then begin
           let _,f = find_file_in_path (Library.get_load_path ())
             (make_suffix fname ".v") in
-          chan_translate:=open_out (f^"8")
+          chan_translate := open_out (f^"8");
+          Pp.comments := []
         end;
         begin try
           read_vernac_file verbosely (make_suffix fname ".v");
           if Options.do_translate () then close_out !chan_translate;
-          chan_translate := ch
+          chan_translate := ch;
+          Lexer.restore_com_state cs;
+          Pp.comments := cl
         with e ->
-          if Options.do_translate () then close_out !chan_translate;
+          if Options.do_translate() then close_out !chan_translate;
           chan_translate := ch;
-	  raise e end;
+          Lexer.restore_com_state cs;
+          Pp.comments := cl;
+          raise e end;
 
     | VernacList l -> List.iter (fun (_,v) -> interp v) l
 
@@ -133,7 +163,9 @@ let rec vernac_com interpfun (loc,com) =
 
     (* To be interpreted in v7 or translator input only *)
     | VernacV7only v ->
-        if !Options.v7 || Options.do_translate() then interp v
+        Options.v7_only := true;
+        if !Options.v7 || Options.do_translate() then interp v;
+        Options.v7_only := false
 
     (* To be interpreted in translator output only *)
     | VernacV8only v -> 
@@ -145,32 +177,11 @@ let rec vernac_com interpfun (loc,com) =
   in 
   try
     Options.v7_only := false;
-    if do_translate () then
-      (Format.set_formatter_out_channel !chan_translate;
-       Format.set_max_boxes max_int;
-       (match com with
-         | VernacV7only _ ->
-             Options.v7_only := true;
-             if !translate_file then msg (pr_comments !comments)
-	 | VernacNop ->
-             if !translate_file then msg (pr_comments !comments)
-         | _ ->
-	     let fs = States.freeze () in
-             let p = pr_vernac com in
-             if !translate_file then
-               msgnl (pr_comments !comments ++ hov 0 p)
-             else
-	       (msgnl
-                 (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++
-                         p)));
-	     States.unfreeze fs);
-       Constrintern.set_temporary_implicits_in [];
-       Constrextern.set_temporary_implicits_out [];
-       comments := None;
-       Format.set_formatter_out_channel stdout);
+    if do_translate () then pr_new_syntax loc (Some com);
     interp com;
   with e -> 
     Format.set_formatter_out_channel stdout;
+    Options.v7_only := false;
     raise (DuringCommandInterp (loc, e))
 
 and vernac interpfun input =
@@ -192,7 +203,8 @@ and read_vernac_file verbosely s =
     Format.set_formatter_out_channel stdout;
     close_input in_chan input;    (* we must close the file first *)
     match real_error e with
-      | End_of_input -> ()
+      | End_of_input ->
+          if do_translate () then pr_new_syntax (max_int,max_int) None
       | _ -> raise_with_file fname e
 
 (* raw_do_vernac : char Stream.t -> unit
@@ -229,14 +241,10 @@ let compile verbosely f =
 *)
   let ldir,long_f_dot_v = Library.start_library f in
   if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
-  if Options.do_translate () then chan_translate := open_out (f^".v8");
+  chan_translate :=
+    if Options.do_translate () then open_out (f^".v8") else stdout;
   let _ = load_vernac verbosely long_f_dot_v in
-  if Options.do_translate () then begin
-    Format.set_formatter_out_channel !chan_translate;
-    msg (pr_comments !comments);
-    Format.set_formatter_out_channel stdout;
-    close_out !chan_translate
-  end;
+  if Options.do_translate () then close_out !chan_translate;
   if Pfedit.get_all_proof_names () <> [] then
     (message "Error: There are pending proofs"; exit 1);
   Library.save_library_to ldir (long_f_dot_v ^ "o")
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 784c977dd8..5e5a3236b4 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -74,6 +74,8 @@ let pr_notation pr s env =
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
+let surround p = str"(" ++ p ++ str")"
+
 open Rawterm
 
 let pr_opt pr = function
@@ -106,7 +108,15 @@ let pr_name = function
   | Anonymous -> str"_"
   | Name id -> pr_id (Constrextern.v7_to_v8_id id)
 
-let pr_located pr (loc,x) = pr x
+let pr_located pr ((b,e),x) =
+  if Options.do_translate() then comment b ++ pr x ++ comment e
+  else pr x
+
+let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
+
+let pr_or_var pr = function
+  | Genarg.ArgArg x -> pr x
+  | Genarg.ArgVar (loc,s) -> pr_with_comments loc (pr_id s)
 
 let las = 12
 
@@ -124,16 +134,15 @@ let rec pr_patt inh p =
   | CPatDelimiters (_,k,p) ->
       pr_delimiters k (pr_patt (latom,E) p), latom
   in
-  if prec_less prec inh then strm
-  else str"(" ++ strm ++ str")"
+  let loc = cases_pattern_loc p in
+  pr_with_comments loc (if prec_less prec inh then strm else surround strm)
 
-let pr_eqn pr (_,pl,rhs) =
+let pr_eqn pr (loc,pl,rhs) =
   spc() ++ hov 4
-    (str "| " ++
-     hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++
-     spc() ++ pr ltop rhs)
-
-let surround p = str"(" ++ p ++ str")"
+    (pr_with_comments loc
+      (str "| " ++
+      hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++
+      spc() ++ pr ltop rhs))
 
 let pr_binder many pr (nal,t) =
   match t with
@@ -371,13 +380,39 @@ let pr_app pr a l =
     pr (lapp,L) a  ++ 
     prlist (fun a -> spc () ++ pr_expl_args pr a) l)
 
+
+let cs = function
+  | CRef(Ident(_,i)) -> "ID"
+  | CRef(Qualid(_,q)) -> "Q"
+  | CFix(_,x,a) -> "FX"
+  | CCoFix(_,x,a) -> "CFX"
+  | CArrow(_,a,b) -> "->"
+  | CProdN(_,bl,a) -> "Pi"
+  | CLambdaN(_,bl,a) -> "L"
+  | CLetIn(_,x,a,b) -> "LET"
+  | CAppExpl(_,f,a) -> "@E"
+  | CApp(_,f,a) -> "@"
+  | CCases(_,p,a,br) -> "C"
+  | COrderedCase(_,s,p,a,br) -> "OC"
+  | CLetTuple(_,ids,p,a,b) -> "LC"
+  | CIf(_,e,p,a,b) -> "LI"
+  | CHole _ -> "?"
+  | CPatVar(_,v) -> "PV"
+  | CEvar(_,ev) -> "EV"
+  | CSort(_,s) -> "S"
+  | CCast(_,a,b) -> "::"
+  | CNotation(_,n,l) -> "NOT"
+  | CNumeral(_,i) -> "NUM"
+  | CDelimiters(_,s,e) -> "DEL"
+  | CDynamic(_,d) -> "DYN"
+
 let rec pr inherited a =
   let (strm,prec) = match a with
   | CRef r -> pr_reference r, latom
   | CFix (_,id,fix) ->
       let p = hov 0 (str"fix " ++ pr_recursive (pr_fixdecl pr) (snd id) fix) in
       (if List.length fix = 1 & prec_less (fst inherited) ltop
-       then str"(" ++ p ++ str")" else p),
+       then surround p else p),
       lfix
   | CCoFix (_,id,cofix) ->
       hov 0 (str "cofix " ++ pr_recursive (pr_cofixdecl pr) (snd id) cofix),
@@ -494,8 +529,9 @@ let rec pr inherited a =
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr (latom,E) a), latom
   | CDynamic _ -> str "<dynamic>", latom
   in
-  if prec_less prec inherited then strm
-  else str"(" ++ strm ++ str")"
+  let loc = constr_loc a in
+  pr_with_comments loc
+    (if prec_less prec inherited then strm else surround strm)
 
 let rec strip_context n iscast t =
   if n = 0 then
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 6952bed566..0cd5dcd3fa 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -38,9 +38,14 @@ val prec_less : int -> int * Ppextend.parenRelation -> bool
 val pr_global : Idset.t -> global_reference -> std_ppcmds
  
 val pr_tight_coma : unit -> std_ppcmds
+val pr_located :
+  ('a -> std_ppcmds) -> 'a located -> std_ppcmds
+val pr_with_comments : loc -> std_ppcmds -> std_ppcmds
 val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
+val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+val pr_metaid : identifier -> std_ppcmds
 val pr_red_expr :
   ('a -> std_ppcmds) * ('a -> std_ppcmds) *  ('b -> std_ppcmds) ->
     ('a,'b) red_expr_gen -> std_ppcmds
@@ -59,7 +64,6 @@ val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
 val pr_may_eval :
   ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval
     -> std_ppcmds
-val pr_metaid : identifier -> std_ppcmds
 
 val pr_rawconstr_env : env -> rawconstr -> std_ppcmds
 val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index f82c227438..574b665019 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -23,6 +23,19 @@ open Genarg
 open Libnames
 open Pptactic
 
+(* In v8 syntax only double quote char is escaped by repeating it *)
+let rec escape_string_v8 s =
+  let rec escape_at s i =
+    if i<0 then s
+    else if s.[i] == '"' then
+      let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
+      escape_at s' (i-1)
+    else escape_at s (i-1) in
+  escape_at s (String.length s - 1)
+
+let qstringnew s = str ("\""^escape_string_v8 s^"\"")
+let qsnew = qstringnew
+
 let translate_v7_ltac = function
   | "DiscrR" -> "discrR"
   | "Sup0" -> "prove_sup0"
@@ -106,7 +119,7 @@ let id_of_ltac_v7_id id =
 
 let pr_ltac_or_var pr = function
   | ArgArg x -> pr x
-  | ArgVar (_,id) -> pr_id (id_of_ltac_v7_id id)
+  | ArgVar (loc,id) -> pr_with_comments loc ( pr_id (id_of_ltac_v7_id id))
 
 let pr_id id = pr_id (Constrextern.v7_to_v8_id id)
 
@@ -191,7 +204,7 @@ let pr_clause_pattern pr_id = function
 
 let pr_induction_arg prc = function
   | ElimOnConstr c -> prc c
-  | ElimOnIdent (_,id) -> pr_id id
+  | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
   | ElimOnAnonHyp n -> int n
 
 let pr_match_pattern pr_pat = function
@@ -200,7 +213,7 @@ let pr_match_pattern pr_pat = function
   | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]"
 
 let pr_match_hyps pr_pat = function
-  | Hyp ((_,na),mp) -> pr_name na ++ str ":" ++ pr_match_pattern pr_pat mp
+  | Hyp (nal,mp) -> pr_located pr_name nal ++ str ":" ++ pr_match_pattern pr_pat mp
 
 let pr_match_rule m pr pr_pat = function
   | Pat ([],mp,t) when m ->
@@ -217,11 +230,11 @@ let pr_funvar = function
   | Some id -> spc () ++ pr_id id
 
 let pr_let_clause k pr prc pr_cst = function
-  | ((_,id),None,t) ->
-      hov 0 (str k ++ pr_id id ++ str " :=" ++ brk (1,1) ++
+  | (id,None,t) ->
+      hov 0 (str k ++ pr_located pr_id id ++ str " :=" ++ brk (1,1) ++
              pr (TacArg t))
-  | ((_,id),Some c,t) ->
-      hv 0 (str k ++ pr_id id ++ str" :" ++ brk(1,2) ++
+  | (id,Some c,t) ->
+      hv 0 (str k ++ pr_located pr_id id ++ str" :" ++ brk(1,2) ++
       pr_may_eval prc prc pr_cst c ++
       str " :=" ++ brk (1,1) ++ pr (TacArg t))
 
@@ -232,8 +245,9 @@ let pr_let_clauses pr prc pr_cst = function
          prlist (fun t -> spc () ++ pr_let_clause "with " pr prc pr_cst t) tl)
   | [] -> anomaly "LetIn must declare at least one binding"
 
-let pr_rec_clause pr ((_,id),(l,t)) =
-  hov 0 (pr_id id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
+let pr_rec_clause pr (id,(l,t)) =
+  hov 0
+    (pr_located pr_id id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
 
 let pr_rec_clauses pr l = 
   prlist_with_sep (fun () -> fnl () ++ str "with ") (pr_rec_clause pr) l
@@ -295,10 +309,13 @@ let rec pr_atom0 env = function
 
   (* Main tactic printer *)
 and pr_atom1 env = function
-  | TacExtend (_,s,l) ->
-      pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s l
-  | TacAlias (_,s,l,_) ->
-      pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s (List.map snd l)
+  | TacExtend (loc,s,l) ->
+      pr_with_comments loc 
+        (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s l)
+  | TacAlias (loc,s,l,_) ->
+      pr_with_comments loc
+        (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s
+          (List.map snd l))
 
   (* Basic tactics *)
   | TacIntroPattern [] as t -> pr_atom0 env t
@@ -308,9 +325,10 @@ and pr_atom1 env = function
       hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h)
   | TacIntroMove (None,None) as t -> pr_atom0 env t
   | TacIntroMove (Some id1,None) -> str "intro " ++ pr_id id1
-  | TacIntroMove (ido1,Some (_,id2)) ->
+  | TacIntroMove (ido1,Some id2) ->
       hov 1
-      (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ pr_id id2)
+      (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++
+       pr_located pr_id id2)
   | TacAssumption as t -> pr_atom0 env t
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg env c)
   | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings env cb)
@@ -403,8 +421,10 @@ and pr_atom1 env = function
   | TacAuto (n,db) -> hov 0 (str "auto" ++ pr_opt int n ++ pr_hintbases db)
   | TacAutoTDB None as x -> pr_atom0 env x
   | TacAutoTDB (Some n) -> hov 0 (str "autotdb" ++ spc () ++ int n)
-  | TacDestructHyp (true,(_,id)) -> hov 0 (str "cdhyp" ++ spc () ++ pr_id id)
-  | TacDestructHyp (false,(_,id)) -> hov 0 (str "dhyp" ++ spc () ++ pr_id id)
+  | TacDestructHyp (true,id) ->
+      hov 0 (str "cdhyp" ++ spc () ++ pr_located pr_id id)
+  | TacDestructHyp (false,id) ->
+      hov 0 (str "dhyp" ++ spc () ++ pr_located pr_id id)
   | TacDestructConcl as x -> pr_atom0 env x
   | TacSuperAuto (n,l,b1,b2) ->
       hov 1 (str "superauto" ++ pr_opt int n ++ pr_autoarg_adding l ++ 
@@ -555,21 +575,23 @@ let rec pr_tac env inherited tac =
   | TacFail (0,"") -> str "fail", latom
   | TacFail (n,s) -> 
       str "fail" ++ (if n=0 then mt () else pr_arg int n) ++
-      (if s="" then mt() else str " \"" ++ str s ++ str "\""), latom
+      (if s="" then mt() else qsnew s), latom
   | TacFirst tl ->
       str "first" ++ spc () ++ pr_seq_body (pr_tac env) tl, llet
   | TacSolve tl ->
       str "solve" ++ spc () ++ pr_seq_body (pr_tac env) tl, llet
   | TacId -> str "idtac", latom
-  | TacAtom (_,t) -> hov 1 (pr_atom1 env t), ltatom
+  | TacAtom (loc,t) ->
+      pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
   | TacArg(Tacexp e) -> pr_tac0 env e, latom
   | TacArg(ConstrMayEval (ConstrTerm c)) -> str "'" ++ pr_constr env c, latom
   | TacArg(ConstrMayEval c) ->
       pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
   | TacArg(Integer n) -> int n, latom
-  | TacArg(TacCall(_,f,l)) ->
-      hov 1 (pr_ref f ++ spc () ++
-             prlist_with_sep spc (pr_tacarg env) l),
+  | TacArg(TacCall(loc,f,l)) ->
+      pr_with_comments loc
+        (hov 1 (pr_ref f ++ spc () ++
+         prlist_with_sep spc (pr_tacarg env) l)),
       lcall
   | TacArg a -> pr_tacarg env a, latom
   in
@@ -577,13 +599,14 @@ let rec pr_tac env inherited tac =
   else str"(" ++ strm ++ str")"
 
 and pr_tacarg env = function
-  | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>")
-  | MetaIdArg (_,s) -> str ("$" ^ s)
+  | TacDynamic (loc,t) ->
+      pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
+  | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s))
   | Identifier id -> pr_id id
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
   | ConstrMayEval (ConstrTerm c) -> pr_constr env c
-  | TacFreshId sopt -> str "fresh" ++ pr_opt qstring sopt
+  | TacFreshId sopt -> str "fresh" ++ pr_opt qsnew sopt
   | (ConstrMayEval _|TacCall _|Tacexp _|Integer _) as a ->
       str "'" ++ pr_tac env (latom,E) (TacArg a)
 
diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli
index 4e8e29a539..b6861f8160 100644
--- a/translate/pptacticnew.mli
+++ b/translate/pptacticnew.mli
@@ -15,6 +15,8 @@ open Proof_type
 open Topconstr
 open Names
 
+val qsnew : string -> std_ppcmds
+
 val pr_raw_tactic : Environ.env -> raw_tactic_expr -> std_ppcmds
  
 val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 0f3d54ed5e..81818bb08d 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -36,9 +36,11 @@ let pr_ltac_id id = pr_id (id_of_ltac_v7_id id)
 let pr_module = Libnames.pr_reference
 
 let pr_reference r =
+  let loc = loc_of_reference r in
   try match Nametab.extended_locate (snd (qualid_of_reference r)) with
     | TrueGlobal ref ->
-	pr_reference (Constrextern.extern_reference dummy_loc Idset.empty ref)
+        pr_with_comments loc
+	  (pr_reference (Constrextern.extern_reference loc Idset.empty ref))
     | SyntacticDef kn ->
 	let is_coq_root d =
 	  let d = repr_dirpath d in
@@ -55,19 +57,17 @@ let pr_reference r =
 		  (reference_of_constr (Coqlib.build_coq_eq_data ()).Coqlib.sym)
               | _ -> r)
           else r
-	in pr_reference r
+	in pr_with_comments loc (pr_reference r)
   with Not_found ->
     error_global_not_found (snd (qualid_of_reference r))
 
-let quote str = "\""^str^"\""
-
 let sep_end () = str"."
 
 let start_theorem = ref false
 
 let insert_proof_keyword () =
   if !start_theorem then 
-    (start_theorem := false; str "Proof" ++ sep_end () ++ fnl())
+    (start_theorem := false; hv 0 (str "Proof" ++ sep_end () ++ fnl()))
   else
     mt ()
 
@@ -153,7 +153,7 @@ let pr_production_item = function
 
 let pr_comment pr_c = function
   | CommentConstr c -> pr_c c
-  | CommentString s -> qs s
+  | CommentString s -> qsnew s
   | CommentInt n -> int n
 
 let pr_in_out_modules = function
@@ -176,7 +176,7 @@ let pr_class_rawexpr = function
 
 let pr_option_ref_value = function
   | QualidRefValue id -> pr_reference id
-  | StringRefValue s -> qs s
+  | StringRefValue s -> qsnew s
 
 let pr_printoption a b = match a with
   | Goptions.PrimaryTable table -> str table ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b
@@ -310,7 +310,7 @@ let pr_type_option pr_c = function
 
 let pr_decl_notation =
   pr_opt (fun (ntn,scopt) -> 
-    str "as " ++ str (quote ntn) ++ 
+    str "as " ++ qsnew ntn ++
     pr_opt (fun sc -> str " :" ++ str sc) scopt)
 
 let rec abstract_rawconstr c = function
@@ -415,12 +415,12 @@ let pr_grammar_tactic_rule (name,(s,pil),t) =
 (*
   hov 0 (
   (* str name ++ spc() ++ *)
-  hov 0 (str"[" ++ qs s ++ spc() ++
+  hov 0 (str"[" ++ qsnew s ++ spc() ++
   prlist_with_sep sep pr_production_item pil ++ str"]") ++
   spc() ++ hov 0 (str"->" ++ spc() ++ str"[" ++ pr_raw_tactic t ++ str"]"))
 *)
   hov 2 (str "Tactic Notation" ++ spc() ++ 
-    hov 0 (qs s ++ spc() ++ prlist_with_sep sep pr_production_item pil ++
+    hov 0 (qsnew s ++ spc() ++ prlist_with_sep sep pr_production_item pil ++
     spc() ++ str":= " ++ spc() ++ pr_raw_tactic t))
 
 let pr_box b = let pr_boxkind = function
@@ -434,14 +434,14 @@ in str"<" ++ pr_boxkind b ++ str">"
 let pr_paren_reln_or_extern = function
   | None,L -> str"L"
   | None,E -> str"E"
-  | Some pprim,Any -> qs pprim
-  | Some pprim,Prec p -> qs pprim ++ spc() ++ str":" ++ spc() ++ int p
+  | Some pprim,Any -> qsnew pprim
+  | Some pprim,Prec p -> qsnew pprim ++ spc() ++ str":" ++ spc() ++ int p
   | _ -> mt()
 
 let rec pr_next_hunks = function 
   | UNP_FNL -> str"FNL"
   | UNP_TAB -> str"TAB"
-  | RO c -> qs c
+  | RO c -> qsnew c
   | UNP_BOX (b,ll) -> str"[" ++ pr_box b ++ prlist_with_sep sep pr_next_hunks ll ++ str"]"
   | UNP_BRK (n,m) -> str"[" ++ int n ++ spc() ++ int m ++ str"]"
   | UNP_TBRK (n,m) -> str"[ TBRK" ++ int n ++ spc() ++ int m ++ str"]"
@@ -511,12 +511,13 @@ let rec pr_vernac = function
   | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i
 
   (* State management *)
-  | VernacWriteState s -> str"Write State" ++ spc () ++ qs s
-  | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s
+  | VernacWriteState s -> str"Write State" ++ spc () ++ qsnew s
+  | VernacRestoreState s -> str"Restore State" ++ spc() ++ qsnew s
 
   (* Control *)
   | VernacList l -> hov 2 (str"[" ++ spc() ++ prlist_with_sep (fun _ -> sep_end () ++ fnl() ) (pr_located pr_vernac) l ++ spc() ++ str"]") 
-  | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc()  ++ str "\"" ++ str s ++ str "\""
+  | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
+  ++ spc()) else spc()  ++ qsnew s
   | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
   | VernacVar id -> pr_id id
   
@@ -554,14 +555,14 @@ let rec pr_vernac = function
 	    (match a with None -> [] | Some a -> [SetAssoc a]),s
         | None -> [],s in
       hov 0 (hov 0 (str"Infix " ++ pr_locality local
-      ++ qs s ++ spc() ++ pr_reference q) ++
+      ++ qsnew s ++ spc() ++ pr_reference q) ++
       pr_syntax_modifiers mv8 ++
       (match sn with
     | None -> mt()
     | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
   | VernacDistfix (local,a,p,s,q,sn) ->
       hov 0 (str"Distfix " ++ pr_locality local ++ pr_entry_prec a ++ int p
-        ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with
+        ++ spc() ++ qsnew s ++ spc() ++ pr_reference q ++ (match sn with
     | None -> mt()
     | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
   | VernacNotation (local,c,sl,mv8,opt) ->
@@ -572,7 +573,7 @@ let rec pr_vernac = function
 	let n = String.length s in
 	if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' 
 	then str (String.sub s 1 (n-2))
-	else qs s in
+	else qsnew s in
       hov 2( str"Notation" ++ spc() ++ pr_locality local ++ ps ++
       str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
       (match opt with
@@ -582,7 +583,7 @@ let rec pr_vernac = function
       let (s,l) = match mv8 with
           None -> out_some sl
         | Some ml -> ml in
-      str"Reserved Notation" ++ spc() ++ pr_locality local ++ qs s ++
+      str"Reserved Notation" ++ spc() ++ pr_locality local ++ qsnew s ++
       pr_syntax_modifiers l
 
   (* Gallina *)
@@ -919,20 +920,20 @@ pr_vbinders bl ++ spc())
         | None -> mt()
         | Some false -> str"Implementation" ++ spc()
         | Some true -> str"Specification" ++ spc ()) ++
-      qs f)
+      qsnew f)
   | VernacAddLoadPath (fl,s,d) -> hov 2
       (str"Add" ++
        (if fl then str" Rec " else spc()) ++
-       str"LoadPath" ++ spc() ++ qs s ++
+       str"LoadPath" ++ spc() ++ qsnew s ++
        (match d with 
          | None -> mt()
          | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir)) 
-  | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s
+  | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qsnew s
   | VernacAddMLPath (fl,s) ->
-      str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s
+      str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qsnew s
   | VernacDeclareMLModule l ->
-      hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
-  | VernacChdir s -> str"Cd" ++ pr_opt qs s
+      hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qsnew l)
+  | VernacChdir s -> str"Cd" ++ pr_opt qsnew s
 
   (* Commands *)
   | VernacDeclareTacticDefinition (rc,l) ->
@@ -1051,9 +1052,9 @@ pr_vbinders bl ++ spc())
   | VernacLocate loc -> 
       let pr_locate =function
 	| LocateTerm qid ->  pr_reference qid
-	| LocateFile f -> str"File" ++ spc() ++ qs f
+	| LocateFile f -> str"File" ++ spc() ++ qsnew f
 	| LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid
-	| LocateNotation s -> str ("\""^s^"\"")
+	| LocateNotation s -> qsnew s
       in str"Locate" ++ spc() ++ pr_locate loc
   | VernacComments l ->
       hov 2