premier debugage

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

20 files changed, 232 insertions, 124 deletions

diff --git a/.depend b/.depend
index b5035826f..6f95ece8c 100644
--- a/.depend
+++ b/.depend
@@ -109,8 +109,8 @@ proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
 proofs/macros.cmi: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \
     proofs/proof_trees.cmi proofs/tacmach.cmi 
 proofs/pfedit.cmi: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
-    lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi \
-    kernel/term.cmi 
+    kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi \
+    proofs/tacmach.cmi kernel/term.cmi 
 proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi lib/pp.cmi kernel/sign.cmi lib/stamps.cmi \
     kernel/term.cmi lib/util.cmi 
@@ -154,8 +154,8 @@ toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi kernel/names.cmi \
 toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi 
 toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
-toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
-    kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
+toplevel/himsg.cmi: kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/sign.cmi kernel/type_errors.cmi 
 toplevel/metasyntax.cmi: parsing/coqast.cmi parsing/extend.cmi 
 toplevel/mltop.cmi: library/libobject.cmi 
 toplevel/protectedtoplevel.cmi: lib/pp.cmi 
@@ -193,7 +193,7 @@ dev/top_printers.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
     tactics/elim.cmx kernel/environ.cmx parsing/esyntax.cmx kernel/evd.cmx \
     kernel/generic.cmx kernel/inductive.cmx parsing/lexer.cmx \
     library/libobject.cmx library/library.cmx toplevel/metasyntax.cmx \
-    toplevel/mltop.cmx kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx \
+    toplevel/mltop.cmi kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx \
     parsing/pretty.cmx parsing/printer.cmx proofs/proof_trees.cmx \
     kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx kernel/sosub.cmx \
     library/states.cmx library/summary.cmx lib/system.cmx \
@@ -405,7 +405,7 @@ library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
 parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
     kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
-    kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx lib/util.cmx parsing/ast.cmi 
+    kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/ast.cmi 
 parsing/astterm.cmo: parsing/ast.cmi kernel/closure.cmi parsing/coqast.cmi \
     library/declare.cmi kernel/environ.cmi pretyping/evarutil.cmi \
     kernel/evd.cmi kernel/generic.cmi library/global.cmi library/impargs.cmi \
@@ -416,7 +416,7 @@ parsing/astterm.cmo: parsing/ast.cmi kernel/closure.cmi parsing/coqast.cmi \
 parsing/astterm.cmx: parsing/ast.cmx kernel/closure.cmx parsing/coqast.cmx \
     library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \
     kernel/evd.cmx kernel/generic.cmx library/global.cmx library/impargs.cmx \
-    kernel/names.cmx library/nametab.cmx parsing/pcoq.cmi lib/pp.cmx \
+    kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx \
     pretyping/pretyping.cmx pretyping/rawterm.cmi kernel/reduction.cmx \
     kernel/sign.cmx pretyping/syntax_def.cmx pretyping/tacred.cmx \
     kernel/term.cmx pretyping/typing.cmx lib/util.cmx parsing/astterm.cmi 
@@ -425,27 +425,35 @@ parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi
 parsing/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
     parsing/lexer.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi \
     parsing/egrammar.cmi 
-parsing/egrammar.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \
-    parsing/lexer.cmx parsing/pcoq.cmi lib/pp.cmx lib/util.cmx \
+parsing/egrammar.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \
+    parsing/lexer.cmx parsing/pcoq.cmx lib/pp.cmx lib/util.cmx \
     parsing/egrammar.cmi 
 parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
     lib/gmap.cmi lib/gmapl.cmi lib/pp.cmi lib/util.cmi parsing/esyntax.cmi 
-parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \
+parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \
     lib/gmap.cmx lib/gmapl.cmx lib/pp.cmx lib/util.cmx parsing/esyntax.cmi 
+parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
+    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi 
+parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
+    parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi 
 parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
     parsing/coqast.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \
     lib/pp.cmi lib/util.cmi parsing/g_natsyntax.cmi 
 parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
-    parsing/coqast.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmi \
+    parsing/coqast.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx \
     lib/pp.cmx lib/util.cmx parsing/g_natsyntax.cmi 
 parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
     parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
-    lib/util.cmi 
+    lib/util.cmi parsing/g_zsyntax.cmi 
 parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
-    parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx \
-    lib/util.cmx 
+    parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx \
+    lib/util.cmx parsing/g_zsyntax.cmi 
 parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi 
 parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi 
+parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
+    lib/util.cmi parsing/pcoq.cmi 
+parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
+    lib/util.cmx parsing/pcoq.cmi 
 parsing/pretty.cmo: pretyping/classops.cmi kernel/constant.cmi \
     library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     library/global.cmi library/impargs.cmi kernel/inductive.cmi \
@@ -468,7 +476,7 @@ parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
     kernel/sign.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \
     parsing/printer.cmi 
 parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
-    parsing/esyntax.cmx parsing/extend.cmi library/global.cmx \
+    parsing/esyntax.cmx parsing/extend.cmx library/global.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
     kernel/sign.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
     parsing/printer.cmi 
@@ -612,7 +620,7 @@ proofs/macros.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
     kernel/term.cmi lib/util.cmi proofs/macros.cmi 
 proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx \
-    parsing/pcoq.cmi lib/pp.cmx proofs/proof_trees.cmx library/summary.cmx \
+    parsing/pcoq.cmx lib/pp.cmx proofs/proof_trees.cmx library/summary.cmx \
     kernel/term.cmx lib/util.cmx proofs/macros.cmi 
 proofs/pfedit.cmo: parsing/astterm.cmi kernel/constant.cmi \
     library/declare.cmi lib/edit.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -727,7 +735,7 @@ tactics/pattern.cmo: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \
     lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi kernel/sosub.cmi \
     tactics/stock.cmi kernel/term.cmi lib/util.cmi tactics/pattern.cmi 
 tactics/pattern.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
-    kernel/generic.cmx library/global.cmx kernel/names.cmx parsing/pcoq.cmi \
+    kernel/generic.cmx library/global.cmx kernel/names.cmx parsing/pcoq.cmx \
     lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sosub.cmx \
     tactics/stock.cmx kernel/term.cmx lib/util.cmx tactics/pattern.cmi 
 tactics/stock.cmo: lib/bij.cmi lib/gmap.cmi lib/gmapl.cmi library/library.cmi \
@@ -787,7 +795,7 @@ toplevel/class.cmo: pretyping/classops.cmi kernel/constant.cmi \
 toplevel/class.cmx: pretyping/classops.cmx kernel/constant.cmx \
     library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
     library/global.cmx kernel/inductive.cmx kernel/instantiate.cmx \
-    library/lib.cmx toplevel/metasyntax.cmx kernel/names.cmx parsing/pcoq.cmi \
+    library/lib.cmx toplevel/metasyntax.cmx kernel/names.cmx parsing/pcoq.cmx \
     lib/pp.cmx pretyping/retyping.cmx kernel/term.cmx pretyping/typing.cmx \
     lib/util.cmx toplevel/class.cmi 
 toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/constant.cmi \
@@ -807,7 +815,7 @@ toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/constant.cmx \
 toplevel/coqinit.cmo: config/coq_config.cmi toplevel/mltop.cmi \
     lib/options.cmi lib/pp.cmi lib/system.cmi toplevel/toplevel.cmi \
     toplevel/vernac.cmi toplevel/coqinit.cmi 
-toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmx \
+toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmi \
     lib/options.cmx lib/pp.cmx lib/system.cmx toplevel/toplevel.cmx \
     toplevel/vernac.cmx toplevel/coqinit.cmi 
 toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
@@ -816,14 +824,16 @@ toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
     library/states.cmi lib/system.cmi toplevel/toplevel.cmi \
     toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi 
 toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \
-    toplevel/errors.cmx library/library.cmx toplevel/mltop.cmx \
+    toplevel/errors.cmx library/library.cmx toplevel/mltop.cmi \
     lib/options.cmx lib/pp.cmx parsing/printer.cmx lib/profile.cmx \
     library/states.cmx lib/system.cmx toplevel/toplevel.cmx \
     toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx 
-toplevel/errors.cmo: parsing/ast.cmi toplevel/himsg.cmi lib/options.cmi \
-    lib/pp.cmi kernel/type_errors.cmi lib/util.cmi toplevel/errors.cmi 
-toplevel/errors.cmx: parsing/ast.cmx toplevel/himsg.cmx lib/options.cmx \
-    lib/pp.cmx kernel/type_errors.cmx lib/util.cmx toplevel/errors.cmi 
+toplevel/errors.cmo: parsing/ast.cmi toplevel/himsg.cmi kernel/inductive.cmi \
+    lib/options.cmi lib/pp.cmi kernel/type_errors.cmi lib/util.cmi \
+    toplevel/errors.cmi 
+toplevel/errors.cmx: parsing/ast.cmx toplevel/himsg.cmx kernel/inductive.cmx \
+    lib/options.cmx lib/pp.cmx kernel/type_errors.cmx lib/util.cmx \
+    toplevel/errors.cmi 
 toplevel/fhimsg.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
     lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi 
@@ -831,22 +841,24 @@ toplevel/fhimsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
     lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx lib/util.cmx toplevel/fhimsg.cmi 
 toplevel/himsg.cmo: parsing/ast.cmi kernel/environ.cmi kernel/generic.cmi \
-    kernel/names.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \
-    kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/type_errors.cmi lib/util.cmi toplevel/himsg.cmi 
+    kernel/inductive.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
+    parsing/pretty.cmi parsing/printer.cmi kernel/reduction.cmi \
+    kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi lib/util.cmi \
+    toplevel/himsg.cmi 
 toplevel/himsg.cmx: parsing/ast.cmx kernel/environ.cmx kernel/generic.cmx \
-    kernel/names.cmx lib/options.cmx lib/pp.cmx parsing/printer.cmx \
-    kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi 
+    kernel/inductive.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
+    parsing/pretty.cmx parsing/printer.cmx kernel/reduction.cmx \
+    kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmx lib/util.cmx \
+    toplevel/himsg.cmi 
 toplevel/metasyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \
     parsing/egrammar.cmi parsing/esyntax.cmi parsing/extend.cmi \
     library/lib.cmi library/libobject.cmi library/library.cmi \
     parsing/pcoq.cmi lib/pp.cmi library/summary.cmi lib/util.cmi \
     toplevel/metasyntax.cmi 
 toplevel/metasyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    parsing/egrammar.cmx parsing/esyntax.cmx parsing/extend.cmi \
+    parsing/egrammar.cmx parsing/esyntax.cmx parsing/extend.cmx \
     library/lib.cmx library/libobject.cmx library/library.cmx \
-    parsing/pcoq.cmi lib/pp.cmx library/summary.cmx lib/util.cmx \
+    parsing/pcoq.cmx lib/pp.cmx library/summary.cmx lib/util.cmx \
     toplevel/metasyntax.cmi 
 toplevel/minicoq.cmo: kernel/constant.cmi toplevel/fhimsg.cmi \
     parsing/g_minicoq.cmi kernel/generic.cmi kernel/inductive.cmi \
@@ -856,16 +868,10 @@ toplevel/minicoq.cmx: kernel/constant.cmx toplevel/fhimsg.cmx \
     parsing/g_minicoq.cmi kernel/generic.cmx kernel/inductive.cmx \
     kernel/names.cmx lib/pp.cmx kernel/safe_typing.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/type_errors.cmx lib/util.cmx 
-toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
-    lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi toplevel/mltop.cmi 
-toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \
-    lib/pp.cmx library/summary.cmx lib/system.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx toplevel/mltop.cmi 
 toplevel/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \
     lib/pp.cmi toplevel/vernac.cmi toplevel/vernacinterp.cmi \
     toplevel/protectedtoplevel.cmi 
-toplevel/protectedtoplevel.cmx: toplevel/errors.cmx parsing/pcoq.cmi \
+toplevel/protectedtoplevel.cmx: toplevel/errors.cmx parsing/pcoq.cmx \
     lib/pp.cmx toplevel/vernac.cmx toplevel/vernacinterp.cmx \
     toplevel/protectedtoplevel.cmi 
 toplevel/record.cmo: parsing/ast.cmi toplevel/class.cmi parsing/coqast.cmi \
@@ -878,8 +884,8 @@ toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi toplevel/mltop.cmi \
     lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
     toplevel/protectedtoplevel.cmi lib/util.cmi toplevel/vernac.cmi \
     toplevel/vernacinterp.cmi toplevel/toplevel.cmi 
-toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmx \
-    lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx lib/pp.cmx \
+toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \
+    lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
     toplevel/protectedtoplevel.cmx lib/util.cmx toplevel/vernac.cmx \
     toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: toplevel/usage.cmi 
@@ -889,7 +895,7 @@ toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
     library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
     toplevel/vernac.cmi 
 toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
-    lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx lib/pp.cmx \
+    lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
     library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
@@ -908,10 +914,10 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
 toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
     toplevel/class.cmx toplevel/command.cmx parsing/coqast.cmx \
     library/declare.cmx library/discharge.cmx kernel/environ.cmx \
-    kernel/evd.cmx parsing/extend.cmi library/global.cmx library/goptions.cmx \
+    kernel/evd.cmx parsing/extend.cmx library/global.cmx library/goptions.cmx \
     library/impargs.cmx library/lib.cmx library/libobject.cmx \
     library/library.cmx proofs/macros.cmx toplevel/metasyntax.cmx \
-    kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmi \
+    kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmx \
     proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \
     parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \
     proofs/refiner.cmx lib/stamps.cmx library/states.cmx lib/system.cmx \
diff --git a/.depend.camlp4 b/.depend.camlp4
index 21f83048d..68d5393d3 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -1,19 +1,17 @@
 parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
-    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi toplevel/vernac.cmi \
-    parsing/extend.cmi 
+    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi 
 parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
-    parsing/pcoq.cmi lib/pp.cmx lib/util.cmx toplevel/vernac.cmx \
-    parsing/extend.cmi 
+    parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi 
 parsing/g_basevernac.cmo: parsing/ast.cmi toplevel/command.cmi \
     parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi 
 parsing/g_basevernac.cmx: parsing/ast.cmx toplevel/command.cmx \
-    parsing/coqast.cmx parsing/pcoq.cmi toplevel/vernac.cmx 
+    parsing/coqast.cmx parsing/pcoq.cmx toplevel/vernac.cmx 
 parsing/g_cases.cmo: toplevel/command.cmi parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_cases.cmx: toplevel/command.cmx parsing/coqast.cmx parsing/pcoq.cmi 
+parsing/g_cases.cmx: toplevel/command.cmx parsing/coqast.cmx parsing/pcoq.cmx 
 parsing/g_command.cmo: parsing/ast.cmi toplevel/command.cmi \
     parsing/coqast.cmi parsing/pcoq.cmi 
 parsing/g_command.cmx: parsing/ast.cmx toplevel/command.cmx \
-    parsing/coqast.cmx parsing/pcoq.cmi 
+    parsing/coqast.cmx parsing/pcoq.cmx 
 parsing/g_minicoq.cmo: kernel/generic.cmi parsing/lexer.cmi kernel/names.cmi \
     lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
     parsing/g_minicoq.cmi 
@@ -21,18 +19,24 @@ parsing/g_minicoq.cmx: kernel/generic.cmx parsing/lexer.cmx kernel/names.cmx \
     lib/pp.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
     parsing/g_minicoq.cmi 
 parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
+parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
 parsing/g_tactic.cmo: parsing/ast.cmi toplevel/command.cmi parsing/coqast.cmi \
     parsing/pcoq.cmi lib/pp.cmi lib/util.cmi 
 parsing/g_tactic.cmx: parsing/ast.cmx toplevel/command.cmx parsing/coqast.cmx \
-    parsing/pcoq.cmi lib/pp.cmx lib/util.cmx 
+    parsing/pcoq.cmx lib/pp.cmx lib/util.cmx 
 parsing/g_vernac.cmo: toplevel/command.cmi parsing/coqast.cmi \
     parsing/pcoq.cmi toplevel/vernac.cmi 
 parsing/g_vernac.cmx: toplevel/command.cmx parsing/coqast.cmx \
-    parsing/pcoq.cmi toplevel/vernac.cmx 
+    parsing/pcoq.cmx toplevel/vernac.cmx 
 parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
     lib/util.cmi parsing/pcoq.cmi 
 parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
     lib/util.cmx parsing/pcoq.cmi 
 parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
 parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
+toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
+    lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \
+    toplevel/vernacinterp.cmi toplevel/mltop.cmi 
+toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \
+    lib/pp.cmx library/summary.cmx lib/system.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmx toplevel/mltop.cmi 
diff --git a/Makefile b/Makefile
index 15d3839b0..05659ece6 100644
--- a/Makefile
+++ b/Makefile
@@ -154,6 +154,13 @@ parsing: $(PARSING)
 pretyping: $(PRETYPING)
 toplevel: $(TOPLEVEL)
 
+# states
+
+SYNTAXPP=syntax/PPCommand.v syntax/PPTactic.v syntax/PPMultipleCase.v
+
+states/barestate.coq: $(SYNTAXPP) coqtop.byte
+	./coqtop.byte -q -batch -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq
+
 ###########################################################################
 # minicoq
 ###########################################################################
@@ -256,7 +263,14 @@ parsing/extend.cmx: parsing/extend.ml4 parsing/grammar.cma
 
 beforedepend:: $(GRAMMARCMO)
 
-# toplevel/mltop.ml4 (ifdef Opt)
+parsing/pcoq.ml: parsing/pcoq.ml4
+	$(CAMLP4EXTEND) pr_o.cmo -impl $< -o $@
+parsing/extend.ml: parsing/extend.ml4 parsing/grammar.cma
+	$(CAMLP4GRAMMAR) pr_o.cmo -impl $< -o $@
+
+beforedepend:: parsing/pcoq.ml parsing/extend.ml
+
+# toplevel/mltop.ml4 (ifdef Byte)
 
 CAMLP4IFDEF=camlp4o pa_ifdef.cmo
 
@@ -303,6 +317,7 @@ archclean::
 	rm -f parsing/*.cmx parsing/*.[so]
 	rm -f pretyping/*.cmx pretyping/*.[so]
 	rm -f toplevel/*.cmx toplevel/*.[so]
+	rm -f coqtop coqtop.byte minicoq
 
 cleanall:: archclean
 	rm -f *~
@@ -333,7 +348,7 @@ dependcamlp4: beforedepend
 	rm -f .depend.camlp4
 	for f in */*.ml4; do \
 	  file=`dirname $$f`/`basename $$f .ml4`; \
-	  camlp4o $(INCLUDES) pa_extend.cmo q_MLast.cmo $(GRAMMARCMO) pr_o.cmo -impl $$f > $$file.ml; \
+	  camlp4o $(INCLUDES) pa_ifdef.cmo pa_extend.cmo q_MLast.cmo $(GRAMMARCMO) pr_o.cmo -impl $$f > $$file.ml; \
 	  ocamldep $(DEPFLAGS) $$file.ml >> .depend.camlp4; \
 	  rm -f $$file.ml; \
 	done
diff --git a/dev/changements.txt b/dev/changements.txt
index 92251833f..538424d7f 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -71,3 +71,17 @@ Changements dans les grammaires
                                  casse particulière dans Coq)
 		
 	
+Changements divers
+------------------
+
+ . il n'y a plus de script coqtop => coqtop et coqtop.byte sont
+   directement le résultat du link du code
+   => debuggage et profiling directs
+
+ . il n'y a plus d'installation locale dans bin/
+ 
+ . #use "include.ml"  =>  #use "include"
+   go()               =>  loop()
+
+ . il y "make depend" et "make dependcamlp4" car ce dernier prend beaucoup
+   de temps
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0131df8b9..c53c46233 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -881,7 +881,7 @@ let clenv_type_of ce c =
          | (n,Cltyp typ)    -> (n,typ.rebus))
       (intmap_to_list ce.env)
   in
-  failwith "TODO"
+  failwith "clenv_type_of: TODO"
   (***
   (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap
      (gLOB(w_hyps ce.hook)) c).uj_type
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9fc376855..6e6114f90 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -228,7 +228,7 @@ let abort_refine f x =
   f x
   (* used to be: error "Must save or abort current goal first" *)
 
-let reset_name = abort_refine reset_to
+let reset_name = abort_refine reset_name
 (*** TODO 
 and reset_keeping_name = abort_refine reset_keeping
 and reset_section = abort_refine raw_reset_section
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 966630eae..9a528f555 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -3,6 +3,7 @@
 
 (*i*)
 open Pp
+open Names
 open Term
 open Sign
 open Environ
@@ -50,6 +51,7 @@ val proof_term : unit -> constr
 
 val start_proof : string -> strength -> Coqast.t -> unit
 val start_proof_constr : string -> strength -> constr -> unit
+val reset_name : identifier -> unit
 
 val save_named : bool -> unit
 val save_anonymous : bool -> string -> 'a -> unit
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 01a2d5f6d..333aca134 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -17,9 +17,7 @@ type auto_tactic =
   | Give_exact of constr                  
   | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
   | Unfold_nth of constr                 (* Hint Unfold *)
-  (***TODO
-  | Extern     of CoqAst.t               (* Hint Extern *)
-  ***)
+  | Extern     of Coqast.t               (* Hint Extern *)
 
 type pri_auto_tactic = { 
   hname : identifier;     (* name of the hint *)
@@ -87,10 +85,8 @@ val make_resolve_hyp : identifier -> constr -> (constr * pri_auto_tactic) list
 
 (* [make_extern name pri pattern tactic_ast] *)
 
-(***TODO
 val make_extern :
-  identifier -> int -> constr -> CoqAst.t -> constr * pri_auto_tactic
-***)
+  identifier -> int -> constr -> Coqast.t -> constr * pri_auto_tactic
 
 (* Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints *)
diff --git a/tactics/pattern.ml b/tactics/pattern.ml
index 52b6586b5..5ff9a6294 100644
--- a/tactics/pattern.ml
+++ b/tactics/pattern.ml
@@ -28,12 +28,9 @@ let rec whd_replmeta = function
   | DOP2(Cast,c,_) -> whd_replmeta c
   | c -> c
 
-let raw_sopattern_of_compattern sign com =
-  failwith "raw_sopattern_of_compattern: TODO"
-  (***
-  let c = Astterm.raw_constr_of_compattern Evd.empty (gLOB sign) com in
-  strong whd_replmeta c
-  ***)
+let raw_sopattern_of_compattern env com =
+  let c = Astterm.constr_of_com_pattern Evd.empty env com in
+  strong (fun _ _ -> whd_replmeta) env Evd.empty c
 
 let parse_pattern s =
   let com =
@@ -42,7 +39,7 @@ let parse_pattern s =
     with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
       error "Malformed pattern" 
   in
-  raw_sopattern_of_compattern (Global.context()) com
+  raw_sopattern_of_compattern (Global.env()) com
     
 let (pattern_stock : constr Stock.stock) =
   Stock.make_stock {name="PATTERN";proc=parse_pattern}
diff --git a/tactics/pattern.mli b/tactics/pattern.mli
index fc9d07ef7..afe1ec848 100644
--- a/tactics/pattern.mli
+++ b/tactics/pattern.mli
@@ -47,9 +47,7 @@ val put_pat            : module_mark -> string -> marked_term
 val get_pat            : marked_term -> constr
 val pattern_stock      : constr Stock.stock
 
-(*i**
-val raw_sopattern_of_compattern : typed_type signature -> CoqAst.t -> constr
-**i*)
+val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr
 
 (*s Second part : Given a term with second-order variables in it,
    represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6fb962f2c..ff5d324a3 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -16,6 +16,7 @@ open Proof_trees
 open Clenv
 open Pattern
 open Wcclausenv
+open Pretty
 
 (******************************************)
 (*         Basic Tacticals                *)
@@ -197,7 +198,7 @@ let conclPattern concl pat tacast gl =
     List.map 
       (fun (i,c) -> (i, Termast.bdize false (assumptions_for_print []) c))
       constr_bindings in 
-  let tacast' = CoqAst.subst_meta ast_bindings tacast in
+  let tacast' = Coqast.subst_meta ast_bindings tacast in
     Tacinterp.interp tacast' gl
 ***)
 
diff --git a/toplevel/class.ml b/toplevel/class.ml
index dbd088555..35e8e5b87 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -328,12 +328,11 @@ let coercion_syntax idf ps clt =
     | _ -> coercion_syntax_entry idf ps
 
 let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps =
-  let _ = add_anonymous_leaf
-	    (inCoercion
-	       ((coef,
-		 {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}),
-		cls,clt)) 
-  in
+  add_anonymous_leaf
+    (inCoercion
+       ((coef,
+	 {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}),
+	cls,clt));
   coercion_syntax idf ps clt
 
 (* 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c4f4622d7..7ce0d13e8 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -72,19 +72,24 @@ let parameter_def_var ident c =
   declare_parameter (id_of_string ident) c
     
 let hypothesis_def_var is_refining ident n c =
+  let warning () = 
+    mSGERRNL [< 'sTR"Warning: "; 'sTR ident; 
+                'sTR" is declared as a parameter";
+                'sTR" because it is at a global level" >]
+  in
   match n with
-    | NeverDischarge -> parameter_def_var ident c
+    | NeverDischarge -> 
+	warning();
+	parameter_def_var ident c
     | DischargeAt disch_sp ->
         if Lib.is_section_p disch_sp then begin
           declare_variable (id_of_string ident)
              (constr_of_com1 true Evd.empty (Global.env()) c,n,false);
           if is_refining then 
-            mSGERRNL [< 'sTR"Warning: Variable " ; 'sTR ident ; 
+            mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 
                         'sTR" is not visible from current goals" >]
         end else begin
-	  mSGERRNL [< 'sTR"Warning: Declaring " ; 'sTR ident ; 
-                      'sTR" as a parameter rather than a variable " ;
-                      'sTR" because it is at a global level" >];
+	  warning();
           parameter_def_var ident c
 	end
 	  
@@ -109,6 +114,11 @@ let corecursive_message = function
                     'sPC; 'sTR "are corecursively defined">]
 
 let build_mutual lparams lnamearconstrs finite =
+  let allnames = 
+    List.fold_left 
+      (fun acc (id,_,l) -> id::(List.map fst l)@acc) [] lnamearconstrs in
+  if not (list_distinct allnames) then
+    error "Two inductive objects have the same name";
   let lrecnames = List.map (fun (x,_,_)->x)  lnamearconstrs
   and nparams = List.length lparams
   and sigma = Evd.empty 
@@ -142,8 +152,8 @@ let build_mutual lparams lnamearconstrs finite =
       mind_entry_finite = finite;
       mind_entry_inds = mispecvec }
     in
-    declare_mind mie;
     States.unfreeze fs;
+    declare_mind mie;
     pPNL(minductive_message lrecnames)
   with e ->
     States.unfreeze fs; raise e
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index 4029437bf..444d18b42 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -4,6 +4,7 @@
 open Pp
 open Util
 open Ast
+open Inductive
 open Type_errors
 
 let print_loc loc =
@@ -48,6 +49,8 @@ let rec explain_exn_default = function
 
   | TypeError(k,ctx,te) -> Himsg.explain_type_error k ctx te
 
+  | InductiveError e -> Himsg.explain_inductive_error e
+
   | Stdpp.Exc_located (loc,exc) ->
       hOV 0 [< if loc = Ast.dummy_loc then [<>]
                else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >];
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index c47c0abc4..97d61ef38 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -7,10 +7,12 @@ open Options
 open Names
 open Generic
 open Term
+open Inductive
 open Sign
 open Environ
 open Type_errors
 open Reduction
+open Pretty
 open Printer
 open Ast
 
@@ -176,28 +178,28 @@ let explain_cant_find_case_type k ctx c =
   let pe = gentermpr k ctx c in
   hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 'wS 1; pe >]
 
+(***
 let explain_cant_find_case_type_loc loc k ctx c =
   let pe = gentermpr k ctx c in
   user_err_loc
     (loc,"pretype",
      hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 
 	     'wS 1; pe >])
+***)
 
 let explain_occur_check k ctx ev rhs =
   let id = "?" ^ string_of_int ev in
   let pt = gentermpr k ctx rhs in
-  errorlabstrm "Trad.occur_check"
-    [< 'sTR"Occur check failed: tried to define "; 'sTR id;
-      'sTR" with term"; 'bRK(1,1); pt >]
+  [< 'sTR"Occur check failed: tried to define "; 'sTR id;
+     'sTR" with term"; 'bRK(1,1); pt >]
 
 let explain_not_clean k ctx ev t =
   let c = Rel (Intset.choose (free_rels t)) in
   let id = "?" ^ string_of_int ev in
   let var = gentermpr k ctx c in
-  errorlabstrm "Trad.not_clean"
-    [< 'sTR"Tried to define "; 'sTR id;
-       'sTR" with a term using variable "; var; 'sPC;
-       'sTR"which is not in its scope." >]
+  [< 'sTR"Tried to define "; 'sTR id;
+     'sTR" with a term using variable "; var; 'sPC;
+     'sTR"which is not in its scope." >]
 
 let explain_type_error k ctx = function
   | UnboundRel n -> 
@@ -240,20 +242,82 @@ let explain_type_error k ctx = function
       explain_not_clean k ctx n c
 
 let explain_refiner_bad_type k ctx arg ty conclty =
-  errorlabstrm "Logic.conv_leq_goal"
-    [< 'sTR"refiner was given an argument"; 'bRK(1,1); 
-       gentermpr k ctx arg; 'sPC;
-       'sTR"of type"; 'bRK(1,1); gentermpr k ctx ty; 'sPC;
-       'sTR"instead of"; 'bRK(1,1); gentermpr k ctx conclty >]
+  [< 'sTR"refiner was given an argument"; 'bRK(1,1); 
+     gentermpr k ctx arg; 'sPC;
+     'sTR"of type"; 'bRK(1,1); gentermpr k ctx ty; 'sPC;
+     'sTR"instead of"; 'bRK(1,1); gentermpr k ctx conclty >]
 
 let explain_refiner_occur_meta k ctx t =
-  errorlabstrm "Logic.mk_refgoals"
-    [< 'sTR"cannot refine with term"; 'bRK(1,1); gentermpr k ctx t;
-       'sPC; 'sTR"because there are metavariables, and it is";
-       'sPC; 'sTR"neither an application nor a Case" >]
+  [< 'sTR"cannot refine with term"; 'bRK(1,1); gentermpr k ctx t;
+     'sPC; 'sTR"because there are metavariables, and it is";
+     'sPC; 'sTR"neither an application nor a Case" >]
 
 let explain_refiner_cannot_applt k ctx t harg =
-  errorlabstrm "Logic.mkARGGOALS"
-    [< 'sTR"in refiner, a term of type "; 'bRK(1,1);
-       gentermpr k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
-       gentermpr k ctx harg >]
+  [< 'sTR"in refiner, a term of type "; 'bRK(1,1);
+     gentermpr k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
+     gentermpr k ctx harg >]
+
+let explain_refiner_error e =
+  [< 'sTR "TODO: EXPLAIN REFINER ERROR" >]
+
+let error_non_strictly_positive k lna c v  =
+  let env = assumptions_for_print lna in
+  let pc = gentermpr k env c in
+  let pv = gentermpr k env v in
+  [< 'sTR "Non strictly positive occurrence of "; pv; 'sTR " in";
+     'bRK(1,1); pc >]
+
+let error_ill_formed_inductive k lna c v =
+  let env = assumptions_for_print lna in
+  let pc = gentermpr k env c in
+  let pv = gentermpr k env v in
+  [< 'sTR "Not enough arguments applied to the "; pv;
+     'sTR " in"; 'bRK(1,1); pc >]
+
+let error_ill_formed_constructor k lna c v =
+  let env = assumptions_for_print lna in
+  let pc = gentermpr k env c in
+  let pv = gentermpr k env v in
+  [< 'sTR "The conclusion of"; 'bRK(1,1); pc; 'bRK(1,1); 
+     'sTR "is not valid;"; 'bRK(1,1); 'sTR "it must be built from "; pv >]
+
+let str_of_nth n =
+  (string_of_int n)^
+  (match n mod 10 with
+     | 1 -> "st"
+     | 2 -> "nd"
+     | 3 -> "rd"
+     | _ -> "th")
+
+let error_bad_ind_parameters k lna c n v1 v2  =
+  let env = assumptions_for_print lna in
+  let pc = gentermpr k env c in
+  let pv1 = gentermpr k env v1 in
+  let pv2 = gentermpr k env v2 in
+  [< 'sTR ("The "^(str_of_nth n)^" argument of "); pv2; 'bRK(1,1);
+     'sTR "must be "; pv1; 'sTR " in"; 'bRK(1,1); pc >]
+
+let error_same_names_types id =
+  [< 'sTR "The name"; 'sPC; print_id id; 'sPC; 
+     'sTR "is used twice is the inductive types definition." >]
+
+let error_same_names_constructors id cid =
+  [< 'sTR "The constructor name"; 'sPC; print_id cid; 'sPC; 
+     'sTR "is used twice is the definition of type"; 'sPC;
+     print_id id >]
+
+let error_not_an_arity id =
+  [< 'sTR "The type of"; 'sPC; print_id id; 'sPC; 'sTR "is not an arity." >]
+
+let error_bad_entry () =
+  [< 'sTR "Bad inductive definition." >]
+
+let explain_inductive_error = function
+  | NonPos (lna,c,v) -> error_non_strictly_positive CCI lna c v
+  | NotEnoughArgs (lna,c,v) -> error_ill_formed_inductive CCI lna c v
+  | NotConstructor (lna,c,v) -> error_ill_formed_constructor CCI lna c v
+  | NonPar (lna,c,n,v1,v2) -> error_bad_ind_parameters CCI lna c n v1 v2
+  | SameNamesTypes id -> error_same_names_types id
+  | SameNamesConstructors (id,cid) -> error_same_names_constructors id cid
+  | NotAnArity id -> error_not_an_arity id
+  | BadEntry -> error_bad_entry ()
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index ea4c10637..d12d7963e 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -4,12 +4,13 @@
 (*i*)
 open Pp
 open Names
-open Term
+open Inductive
 open Sign
-open Environ
 open Type_errors
 (*i*)
 
 (* This module provides functions to explain the type errors. *)
 
 val explain_type_error : path_kind -> context -> type_error -> std_ppcmds
+
+val explain_inductive_error : inductive_error -> std_ppcmds
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index fbbc48a95..e53dea4de 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -27,7 +27,7 @@ let _ =
 let (inPPSyntax,outPPSyntax) =
   declare_object
     ("PPSYNTAX",
-     { load_function = (fun _ -> ());
+     { load_function = (fun (_,ppobj) -> Esyntax.add_ppobject ppobj);
        open_function = (fun _ -> ());
        cache_function = (fun (_,ppobj) -> Esyntax.add_ppobject ppobj);
        specification_function = (fun x -> x) })
@@ -42,8 +42,8 @@ let ppobj_of_ast whatfor sel =
   (whatfor, List.flatten (List.map (Extend.level_of_ast whatfor) sel))
 
 let add_syntax_obj whatfor sel =
-  let _ = Lib.add_anonymous_leaf (inPPSyntax (ppobj_of_ast whatfor sel)) in
-  ()
+  let ppobj = ppobj_of_ast whatfor sel in
+  Lib.add_anonymous_leaf (inPPSyntax ppobj)
 
 
 (************************
@@ -66,7 +66,7 @@ let (inToken, outToken) =
        cache_function = (fun (_, s) -> Pcoq.lexer.Token.using ("", s));
        specification_function = (fun x -> x)})
 
-let add_token_obj s = let _ = Lib.add_anonymous_leaf (inToken s) in ()
+let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
 (* Grammar rules *)
 let (inGrammar, outGrammar) =
@@ -78,8 +78,7 @@ let (inGrammar, outGrammar) =
        specification_function = (fun x -> x)})
 
 let add_grammar_obj univ al =
-  let _ = Lib.add_anonymous_leaf (inGrammar (Extend.gram_of_ast univ al)) in
-  ()
+   Lib.add_anonymous_leaf (inGrammar (Extend.gram_of_ast univ al))
 
 (* printing grammar entries *)
 let print_grammar univ entry =
@@ -201,8 +200,7 @@ let add_infix assoc n inf pr =
   let gram_rule = gram_infix assoc n (split inf) pr in
   (* check the syntax entry *)
   let syntax_rule = infix_syntax_entry assoc n inf pr in
-  let _ = Lib.add_anonymous_leaf (inInfix(gram_rule,syntax_rule)) in
-  ()
+  Lib.add_anonymous_leaf (inInfix(gram_rule,syntax_rule))
 
 (* Distfix *)
 (* Distfix LEFTA 7 "/ _ / _ /" app.*)
@@ -246,6 +244,5 @@ let distfix assoc n sl f =
   }
 
 let add_distfix a n df f =
-  let _ = Lib.add_anonymous_leaf (inInfix(distfix a n (split df) f, [])) in
-  ()
+  Lib.add_anonymous_leaf (inInfix(distfix a n (split df) f, []))
 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 5329becae..d2a240075 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -224,7 +224,7 @@ let (inMLModule,outMLModule) =
                     specification_function = specification_ml_module_object })
 
 let declare_ml_modules l =
-  let _ = Lib.add_anonymous_leaf (inMLModule {mnames=l}) in ()
+  Lib.add_anonymous_leaf (inMLModule {mnames=l})
     
 let print_ml_path () =
   let l = !coq_mlpath_copy in
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index e78a4b92a..6d2ebf57a 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -203,10 +203,11 @@ let print_toplevel_error exc =
           if valid_buffer_loc top_buffer dloc loc then
             (print_highlight_location top_buffer loc, ie)
           else 
-	    (print_command_location top_buffer dloc, ie)
+	    ([<>] (* print_command_location top_buffer dloc *), ie)
       | Error_in_file (s, (fname, loc), ie) ->
           (print_location_in_file s fname loc, ie)
-      | _ -> (print_command_location top_buffer dloc, exc)
+      | _ -> 
+	  ([<>] (* print_command_location top_buffer dloc *), exc)
   in
   match exc with
     | End_of_input -> 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a01e701bc..17127518c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -254,12 +254,12 @@ let _ =
 	   (fun () -> reset_section (string_of_id id))
        | _ -> bad_vernac_args "ResetSection")
 
+***)
 let _ =
   add "ResetName"
     (function 
-       | [VARG_IDENTIFIER id] -> (fun () -> reset_name id)
+       | [VARG_IDENTIFIER id] -> (fun () -> Pfedit.reset_name id)
        | _ -> bad_vernac_args "ResetName")
-***)
 
 (* Modules *)