separation calcul des implicites et declaration des constantes / inductifs / variables

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

9 files changed, 156 insertions, 124 deletions

diff --git a/.depend b/.depend
index e9498bc0c3..094cc2f805 100644
--- a/.depend
+++ b/.depend
@@ -28,6 +28,8 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
     kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
     library/libobject.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
@@ -46,8 +48,6 @@ library/library.cmi: library/lib.cmi library/nametab.cmi lib/pp.cmi \
 library/nametab.cmi: library/libobject.cmi kernel/names.cmi kernel/term.cmi \
     lib/util.cmi 
 library/summary.cmi: kernel/names.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi 
 parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -187,11 +187,11 @@ toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi
 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/coqast.cmi parsing/pcoq.cmi 
 toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \
     toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     proofs/proof_type.cmi 
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 contrib/xml/xmlcommand.cmi: kernel/names.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
@@ -309,22 +309,30 @@ lib/dyn.cmo: lib/util.cmi lib/dyn.cmi
 lib/dyn.cmx: lib/util.cmx lib/dyn.cmi 
 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/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/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
+lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.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/pp_control.cmo: lib/pp_control.cmi 
+lib/pp_control.cmx: lib/pp_control.cmi 
 lib/profile.cmo: lib/system.cmi lib/profile.cmi 
 lib/profile.cmx: lib/system.cmx lib/profile.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.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: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/evd.cmi library/global.cmi library/impargs.cmi \
     library/indrec.cmi kernel/inductive.cmi library/lib.cmi \
@@ -395,14 +403,6 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
     library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     library/summary.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.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/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 \
@@ -447,12 +447,6 @@ parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi
 parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
 parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
 parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx 
-parsing/g_minicoq.cmo: kernel/environ.cmi parsing/lexer.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
-    parsing/g_minicoq.cmi 
-parsing/g_minicoq.cmx: kernel/environ.cmx parsing/lexer.cmx kernel/names.cmx \
-    lib/pp.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
-    parsing/g_minicoq.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 
@@ -975,10 +969,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
     library/global.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi 
-tools/coqdep_lexer.cmo: config/coq_config.cmi 
-tools/coqdep_lexer.cmx: config/coq_config.cmx 
 tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
 tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coqdep_lexer.cmo: config/coq_config.cmi 
+tools/coqdep_lexer.cmx: config/coq_config.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
 tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \
@@ -1050,7 +1044,7 @@ toplevel/errors.cmx: parsing/ast.cmx toplevel/himsg.cmx kernel/indtypes.cmx \
 toplevel/fhimsg.cmo: kernel/environ.cmi parsing/g_minicoq.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 
-toplevel/fhimsg.cmx: kernel/environ.cmx parsing/g_minicoq.cmx \
+toplevel/fhimsg.cmx: kernel/environ.cmx parsing/g_minicoq.cmi \
     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 library/global.cmi \
@@ -1082,7 +1076,7 @@ toplevel/minicoq.cmo: kernel/declarations.cmi toplevel/fhimsg.cmi \
     kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/type_errors.cmi lib/util.cmi 
 toplevel/minicoq.cmx: kernel/declarations.cmx toplevel/fhimsg.cmx \
-    parsing/g_minicoq.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
+    parsing/g_minicoq.cmi 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/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \
@@ -1113,6 +1107,14 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \
     toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: toplevel/usage.cmi 
 toplevel/usage.cmx: toplevel/usage.cmi 
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi \
+    toplevel/discharge.cmi library/library.cmi lib/options.cmi \
+    parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.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 \
+    toplevel/discharge.cmx library/library.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 \
     toplevel/class.cmi toplevel/command.cmi parsing/coqast.cmi \
     library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \
@@ -1153,14 +1155,6 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
     lib/util.cmx toplevel/vernacinterp.cmi 
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    toplevel/discharge.cmi library/library.cmi lib/options.cmi \
-    parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.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 \
-    toplevel/discharge.cmx library/library.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 
 contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \
     library/declare.cmi kernel/environ.cmi tactics/equality.cmi \
     kernel/evd.cmi library/global.cmi kernel/inductive.cmi proofs/logic.cmi \
@@ -1203,6 +1197,8 @@ contrib/ring/ring.cmx: parsing/astterm.cmx kernel/closure.cmx \
     library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
     tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx 
+contrib/xml/xml.cmo: contrib/xml/xml.cmi 
+contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \
     kernel/evd.cmi library/global.cmi library/lib.cmi library/libobject.cmi \
     library/library.cmi kernel/names.cmi library/nametab.cmi \
@@ -1219,5 +1215,3 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \
     contrib/xml/xmlcommand.cmi 
 contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/xml/xmlcommand.cmx 
-contrib/xml/xml.cmo: contrib/xml/xml.cmi 
-contrib/xml/xml.cmx: contrib/xml/xml.cmi 
diff --git a/.depend.coq b/.depend.coq
index 5dbe990ce6..0ed524ce95 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -1,29 +1,29 @@
+theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo
+theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
+theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
 theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo
 theories/Zarith/Zmisc.vo: theories/Zarith/Zmisc.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Bool/Bool.vo
-theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo
 theories/Zarith/ZArith_dec.vo: theories/Zarith/ZArith_dec.v theories/Bool/Sumbool.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo
-theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo
+theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo
 theories/Zarith/Wf_Z.vo: theories/Zarith/Wf_Z.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo
-theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
-theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
 theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo
-theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v theories/Sets/Relations_1.vo theories/Sets/Relations_2.vo
 theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo
-theories/Sets/Relations_2.vo: theories/Sets/Relations_2.v theories/Sets/Relations_1.vo
+theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v theories/Sets/Relations_1.vo theories/Sets/Relations_2.vo
 theories/Sets/Relations_2_facts.vo: theories/Sets/Relations_2_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo
-theories/Sets/Relations_1.vo: theories/Sets/Relations_1.v
+theories/Sets/Relations_2.vo: theories/Sets/Relations_2.v theories/Sets/Relations_1.vo
 theories/Sets/Relations_1_facts.vo: theories/Sets/Relations_1_facts.v theories/Sets/Relations_1.vo
-theories/Sets/Powerset.vo: theories/Sets/Powerset.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
+theories/Sets/Relations_1.vo: theories/Sets/Relations_1.v
 theories/Sets/Powerset_facts.vo: theories/Sets/Powerset_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo
 theories/Sets/Powerset_Classical_facts.vo: theories/Sets/Powerset_Classical_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo
+theories/Sets/Powerset.vo: theories/Sets/Powerset.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
 theories/Sets/Permut.vo: theories/Sets/Permut.v
 theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo
 theories/Sets/Multiset.vo: theories/Sets/Multiset.v theories/Sets/Permut.vo theories/Arith/Plus.vo
 theories/Sets/Integers.vo: theories/Sets/Integers.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo theories/Sets/Infinite_sets.vo theories/Arith/Compare_dec.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
 theories/Sets/Infinite_sets.vo: theories/Sets/Infinite_sets.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo
 theories/Sets/Image.vo: theories/Sets/Image.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo
-theories/Sets/Finite_sets.vo: theories/Sets/Finite_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo
 theories/Sets/Finite_sets_facts.vo: theories/Sets/Finite_sets_facts.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo
+theories/Sets/Finite_sets.vo: theories/Sets/Finite_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo
 theories/Sets/Ensembles.vo: theories/Sets/Ensembles.v
 theories/Sets/Cpo.vo: theories/Sets/Cpo.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo
 theories/Sets/Constructive_sets.vo: theories/Sets/Constructive_sets.v theories/Sets/Ensembles.vo
@@ -36,37 +36,37 @@ theories/Relations/Operators_Properties.vo: theories/Relations/Operators_Propert
 theories/Relations/Newman.vo: theories/Relations/Newman.v theories/Relations/Rstar.vo
 theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v
 theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Logic/Classical_Prop.vo
-theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
 theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo
 theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rderiv.vo
 theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
 theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo theories/Logic/Classical_Prop.vo contrib/omega/Omega.vo
 theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/Zarith/ZArith.vo theories/Reals/TypeSyntax.vo
-theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v
+theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
 theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v
-theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo
+theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v
 theories/Logic/Classical_Type.vo: theories/Logic/Classical_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
 theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v
 theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo
 theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Prop.vo
+theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo
 theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v theories/Lists/PolyList.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Minus.vo theories/Bool/DecBool.vo
 theories/Lists/Streams.vo: theories/Lists/Streams.v
-theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo
 theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
-theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
+theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo
 theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
+theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
 theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
-theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo
+theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/Wf.vo
 theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo
-theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
-theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo
+theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo
-theories/Init/Datatypes.vo: theories/Init/Datatypes.v
+theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
 theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo
+theories/Init/Datatypes.vo: theories/Init/Datatypes.v
 theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/Bool/Bool.vo
 theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v
 theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo
@@ -76,8 +76,8 @@ theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo
 theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Peano_dec.vo: theories/Arith/Peano_dec.v
 theories/Arith/Mult.vo: theories/Arith/Mult.v theories/Arith/Plus.vo theories/Arith/Minus.vo
-theories/Arith/Min.vo: theories/Arith/Min.v theories/Arith/Arith.vo
 theories/Arith/Minus.vo: theories/Arith/Minus.v theories/Arith/Lt.vo theories/Arith/Le.vo
+theories/Arith/Min.vo: theories/Arith/Min.v theories/Arith/Arith.vo
 theories/Arith/Lt.vo: theories/Arith/Lt.v theories/Arith/Le.vo
 theories/Arith/Le.vo: theories/Arith/Le.v
 theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
@@ -85,28 +85,28 @@ theories/Arith/Even.vo: theories/Arith/Even.v
 theories/Arith/Euclid_proof.vo: theories/Arith/Euclid_proof.v theories/Arith/Minus.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
 theories/Arith/Euclid_def.vo: theories/Arith/Euclid_def.v theories/Arith/Mult.vo
 theories/Arith/EqNat.vo: theories/Arith/EqNat.v
-theories/Arith/Div.vo: theories/Arith/Div.v theories/Arith/Le.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo
 theories/Arith/Div2.vo: theories/Arith/Div2.v theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Compare_dec.vo theories/Arith/Even.vo
-theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
+theories/Arith/Div.vo: theories/Arith/Div.v theories/Arith/Le.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo
 theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo
+theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo
 test-suite/tactics/TestRefine.vo: test-suite/tactics/TestRefine.v tactics/Refine.vo theories/Init/Wf.vo theories/Arith/Wf_nat.vo theories/Arith/Compare_dec.vo theories/Arith/Lt.vo
-test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
 test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
+test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
 contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
 contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/Zarith/ZArith.vo theories/Logic/Eqdep_dec.vo
-contrib/ring/Ring.vo: contrib/ring/Ring.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo contrib/ring/ring.cmo
 contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
 contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
 contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo
+contrib/ring/Ring.vo: contrib/ring/Ring.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo contrib/ring/ring.cmo
 contrib/ring/Quote.vo: contrib/ring/Quote.v contrib/ring/quote.cmo
 contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
 contrib/omega/Zpower.vo: contrib/omega/Zpower.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo
 contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
 contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
-contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo
 contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
+contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo
 tactics/Tauto.vo: tactics/Tauto.v
 tactics/Refine.vo: tactics/Refine.v
 tactics/Inv.vo: tactics/Inv.v tactics/Equality.vo
diff --git a/library/declare.ml b/library/declare.ml
index cf5abce74f..92af415126 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -54,49 +54,39 @@ let _ = Summary.declare_summary "VARIABLE"
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
 	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
 
-let cache_variable (sp,((id,(d,_,_) as vd),imps)) =
+let cache_variable (sp,(id,(d,_,_) as vd)) =
   begin match d with (* Fails if not well-typed *)
     | SectionLocalAssum ty -> Global.push_named_assum (id,ty)
     | SectionLocalDef c -> Global.push_named_def (id,c)
   end;
   Nametab.push id (VarRef sp);
-  if imps then declare_var_implicits sp;
   vartab := Spmap.add sp vd !vartab
 
-let load_variable _ = ()
-
-let open_variable _ = ()
-
-let export_variable x = None
-
 let (in_variable, out_variable) =
   let od = {
     cache_function = cache_variable;
-    load_function = load_variable;
-    open_function = open_variable;
-    export_function = export_variable } in
+    load_function = (fun _ -> ());
+    open_function = (fun _ -> ());
+    export_function = (fun x -> None) }
+  in
   declare_object ("VARIABLE", od)
 
-let out_variable sp = fst (out_variable sp)
-
 let declare_variable id obj =
-  let _ = add_leaf id CCI (in_variable ((id,obj),is_implicit_args())) in
-  ()
+  let sp = add_leaf id CCI (in_variable (id,obj)) in
+  if is_implicit_args() then declare_var_implicits sp
 
 (* Parameters. *)
 
-let cache_parameter (sp,(c,imps)) =
+let cache_parameter (sp,c) =
   Global.add_parameter sp c;
-  Nametab.push (basename sp) (ConstRef sp);
-  if imps then declare_constant_implicits sp
+  Nametab.push (basename sp) (ConstRef sp)
 
-let load_parameter (sp,(_,imps)) =
-  if imps then declare_constant_implicits sp
+let load_parameter _ = ()
 
 let open_parameter (sp,_) =
   Nametab.push (basename sp) (ConstRef sp)
 
-let export_parameter obj = Some obj
+let export_parameter x = Some x
 
 let (in_parameter, out_parameter) =
   let od = {
@@ -108,7 +98,8 @@ let (in_parameter, out_parameter) =
   declare_object ("PARAMETER", od)
 
 let declare_parameter id c =
-  let _ = add_leaf id CCI (in_parameter (c,is_implicit_args())) in ()
+  let sp = add_leaf id CCI (in_parameter c) in 
+  if is_implicit_args() then declare_constant_implicits sp
 
 (* Constants. *)
 
@@ -125,23 +116,21 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.unfreeze_function = (fun ft -> csttab := ft);
 	    Summary.init_function = (fun () -> csttab := Spmap.empty) }
 
-let cache_constant (sp,((cdt,stre),imps)) =
+let cache_constant (sp,(cdt,stre)) =
   begin match cdt with 
     | ConstantEntry ce -> Global.add_constant sp ce
     | ConstantRecipe r -> Global.add_discharged_constant sp r
   end;
   Nametab.push (basename sp) (ConstRef sp);
-  if imps then declare_constant_implicits sp;
   csttab := Spmap.add sp stre !csttab
 
-let load_constant (sp,((ce,stre),imps)) =
-  if imps then declare_constant_implicits sp;
+let load_constant (sp,(ce,stre)) =
   csttab := Spmap.add sp stre !csttab
 
 let open_constant (sp,_) =
   Nametab.push (basename sp) (ConstRef sp)
 
-let export_constant obj = Some obj
+let export_constant x = Some x
 
 let (in_constant, out_constant) =
   let od = {
@@ -153,8 +142,8 @@ let (in_constant, out_constant) =
   declare_object ("CONSTANT", od)
 
 let declare_constant id cd =
-  let _ = add_leaf id CCI (in_constant (cd,is_implicit_args())) in ()
-
+  let sp = add_leaf id CCI (in_constant cd) in
+  if is_implicit_args() then declare_constant_implicits sp
  
 (* Inductives. *)
 
@@ -173,18 +162,16 @@ let push_inductive_names sp mie =
       0 mie.mind_entry_inds
   in ()
 
-let cache_inductive (sp,(mie,imps)) =
+let cache_inductive (sp,mie) =
   Global.add_mind sp mie;
-  push_inductive_names sp mie;
-  if imps then declare_inductive_implicits sp
+  push_inductive_names sp mie
 
-let load_inductive (sp,(_,imps)) =
-  if imps then declare_inductive_implicits sp
+let load_inductive _ = ()
 
-let open_inductive (sp,(mie,_)) =
+let open_inductive (sp,mie) =
   push_inductive_names sp mie
 
-let export_inductive obj = Some obj
+let export_inductive x = Some x
 
 let (in_inductive, out_inductive) =
   let od = {
@@ -200,11 +187,11 @@ let declare_mind mie =
     | (id,_,_,_)::_ -> id
     | [] -> anomaly "cannot declare an empty list of inductives"
   in
-  let sp = add_leaf id CCI (in_inductive (mie,is_implicit_args())) in
+  let sp = add_leaf id CCI (in_inductive mie) in
+  if is_implicit_args() then declare_inductive_implicits sp;
   sp
 
-
-(* Test and access functions. *)
+(*s Test and access functions. *)
 
 let is_constant sp = 
   try let _ = Global.lookup_constant sp in true with Not_found -> false
diff --git a/library/declare.mli b/library/declare.mli
index e1fb407f30..95aa8be8f6 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -44,7 +44,7 @@ val declare_mind : mutual_inductive_entry -> section_path
 
 val declare_eliminations : section_path -> int -> unit
 
-val out_inductive : Libobject.obj -> mutual_inductive_entry * bool
+val out_inductive : Libobject.obj -> mutual_inductive_entry 
 
 val make_strength : string list -> strength
 val make_strength_0 : unit -> strength
diff --git a/library/impargs.ml b/library/impargs.ml
index 5248bc4a61..e2ec4a4762 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -7,6 +7,8 @@ open Reduction
 open Declarations
 open Environ
 open Inductive
+open Libobject
+open Lib
 
 type implicits =
   | Impl_auto of int list
@@ -43,18 +45,30 @@ let list_of_implicits = function
   | Impl_manual l -> l
   | No_impl -> []
 
-(* Constants. *)
+(*s Constants. *)
 
 let constants_table = ref Spmap.empty
 
-let declare_constant_implicits sp =
+let compute_constant_implicits sp =
   let env = Global.env () in
   let cb = lookup_constant sp env in
-  let imps = auto_implicits env (body_of_type cb.const_type) in
+  auto_implicits env (body_of_type cb.const_type)
+
+let cache_constant_implicits (_,(sp,imps)) = 
   constants_table := Spmap.add sp imps !constants_table
 
-let declare_constant_manual_implicits sp imps =
-  constants_table := Spmap.add sp (Impl_manual imps) !constants_table
+let (in_constant_implicits, _) =
+  let od = {
+    cache_function = cache_constant_implicits;
+    load_function = cache_constant_implicits;
+    open_function = (fun _ -> ());
+    export_function = (fun x -> Some x) }
+  in
+  declare_object ("CONSTANT-IMPLICITS", od)
+
+let declare_constant_implicits sp =
+  let imps = compute_constant_implicits sp in
+  add_anonymous_leaf (in_constant_implicits (sp,imps))
 
 let constant_implicits sp =
   try Spmap.find sp !constants_table with Not_found -> No_impl
@@ -62,14 +76,14 @@ let constant_implicits sp =
 let constant_implicits_list sp =
   list_of_implicits (constant_implicits sp)
 
-(* Inductives and constructors. Their implicit arguments are stored
+(*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
    $i$ are the implicit arguments of the inductive and $v$ the array of 
    implicit arguments of the constructors. *)
 
 let inductives_table = ref Spmap.empty
 
-let declare_inductive_implicits sp =
+let compute_inductive_implicits sp =
   let env = Global.env () in
   let mib = lookup_mind sp env in
   let env_ar = push_rels (mind_arities_context mib) env in
@@ -78,9 +92,24 @@ let declare_inductive_implicits sp =
      Array.map (fun c -> auto_implicits env_ar (body_of_type c))
        (mind_user_lc mip))
   in
-  let imps = Array.map imps_one_inductive mib.mind_packets in
+  Array.map imps_one_inductive mib.mind_packets
+
+let cache_inductive_implicits (_,(sp,imps)) =
   inductives_table := Spmap.add sp imps !inductives_table
-    
+
+let (in_inductive_implicits, _) =
+  let od = {
+    cache_function = cache_inductive_implicits;
+    load_function = cache_inductive_implicits;
+    open_function = (fun _ -> ());
+    export_function = (fun x -> Some x) }
+  in
+  declare_object ("INDUCTIVE-IMPLICITS", od)
+ 
+let declare_inductive_implicits sp =
+  let imps = compute_inductive_implicits sp in
+  add_anonymous_leaf (in_inductive_implicits (sp,imps))
+
 let inductive_implicits (sp,i) =
   try
     let imps = Spmap.find sp !inductives_table in fst imps.(i)
@@ -99,20 +128,35 @@ let constructor_implicits_list constr_sp =
 let inductive_implicits_list ind_sp =
   list_of_implicits (inductive_implicits ind_sp)
 
-(* Variables. *)
+(*s Variables. *)
 
 let var_table = ref Spmap.empty
 
-let declare_var_implicits sp =
+let compute_var_implicits sp =
   let env = Global.env () in
   let (_,ty) = lookup_named (basename sp) env in
-  let imps = auto_implicits env (body_of_type ty) in
+  auto_implicits env (body_of_type ty)
+
+let cache_var_implicits (_,(sp,imps)) =
   var_table := Spmap.add sp imps !var_table
 
+let (in_var_implicits, _) =
+  let od = {
+    cache_function = cache_var_implicits;
+    load_function = cache_var_implicits;
+    open_function = (fun _ -> ());
+    export_function = (fun x -> Some x) }
+  in
+  declare_object ("VARIABLE-IMPLICITS", od)
+
+let declare_var_implicits sp =
+  let imps = compute_var_implicits sp in
+  add_anonymous_leaf (in_var_implicits (sp,imps))
+
 let implicits_of_var sp =
   list_of_implicits (try Spmap.find sp !var_table with Not_found -> No_impl)
 
-(* Tests if declared implicit *)
+(*s Tests if declared implicit *)
 
 let is_implicit_constant sp =
   try let _ = Spmap.find sp !constants_table in true with Not_found -> false
@@ -130,7 +174,7 @@ let implicits_of_global = function
   | ConstructRef csp ->	list_of_implicits (constructor_implicits csp)
   | EvarRef _ -> []
 
-(* Registration as global tables and roolback. *)
+(*s Registration as global tables and rollback. *)
 
 type frozen_t = bool
               * implicits Spmap.t 
diff --git a/library/impargs.mli b/library/impargs.mli
index cbe31a3af2..3da01fe090 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -7,8 +7,8 @@ open Term
 open Inductive
 (*i*)
 
-(* Implicit arguments. Here we store the implicit arguments. Notice that we 
-   are outside the kernel, which knows nothing about implicit arguments. *)
+(*s Implicit arguments. Here we store the implicit arguments. Notice that we 
+    are outside the kernel, which knows nothing about implicit arguments. *)
 
 type implicits =
   | Impl_auto of int list
@@ -22,11 +22,15 @@ val with_implicits : bool -> ('a -> 'b) -> 'a -> 'b
 
 val list_of_implicits : implicits -> int list
 
-val declare_constant_implicits : section_path -> unit
-val declare_constant_manual_implicits : section_path -> int list -> unit
-val constant_implicits : section_path -> implicits
+(*s Computation of implicits (done using the global environment). *)
 
+val declare_var_implicits : section_path -> unit
+val declare_constant_implicits : section_path -> unit
 val declare_inductive_implicits : section_path -> unit
+
+(*s Access to already computed implicits. *)
+
+val constant_implicits : section_path -> implicits
 val inductive_implicits : inductive_path -> implicits
 val constructor_implicits : constructor_path -> implicits
 
@@ -34,7 +38,6 @@ val constructor_implicits_list : constructor_path -> int list
 val inductive_implicits_list : inductive_path -> int list
 val constant_implicits_list : section_path -> int list
 
-val declare_var_implicits : section_path -> unit
 val implicits_of_var : section_path -> int list
 
 val is_implicit_constant : section_path -> bool
@@ -43,6 +46,8 @@ val is_implicit_var : section_path -> bool
 
 val implicits_of_global : global_reference -> int list
 
+(*s Rollback. *)
+
 type frozen_t
 val freeze : unit -> frozen_t
 val unfreeze : frozen_t -> unit
diff --git a/library/lib.ml b/library/lib.ml
index b307ee5f55..7d7e9e2c81 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -201,7 +201,6 @@ type frozen = string option * library_segment
 
 let freeze () = (!module_name, !lib_stk)
 
-(* module_name is not set ? *)
 let unfreeze (mn,stk) =
   module_name := mn;
   lib_stk := stk;
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 545c0acb7d..ec1d850e0d 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -114,7 +114,7 @@ Section Logic_lemmas.
     Variable x,y,z : A.
 
     Theorem sym_eq : (eq ? x y) -> (eq ? y x).
-    Proof.
+      Proof.
      Induction 1; Trivial.
     Qed.
 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index f621e5beea..ba584d756e 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -261,7 +261,7 @@ let rec process_object (ccitab, objtab, modtab as tabs) = function
 	| "CONSTANT" | "PARAMETER" ->
             (Idmap.add (basename sp) (ConstRef sp) ccitab,objtab,modtab)
 	| "INDUCTIVE" ->
-	    let mie,_ = out_inductive obj in
+	    let mie = out_inductive obj in
 	    (push_inductive_names ccitab sp mie, objtab, modtab)
         (* Variables are never visible *)
 	| "VARIABLE" -> tabs
@@ -289,10 +289,13 @@ let close_section _ s =
     let newdir = dirpath sec_sp in
     let olddir = wd_of_sp sec_sp in
     let (ops,ids,_) = 
-      List.fold_left (process_item oldenv newdir olddir) ([],[],([],[],[])) decls in 
+      List.fold_left 
+	(process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
+    in 
     Global.pop_named_decls ids;
     List.iter process_operation (List.rev ops);
-    module_contents decls in
+    module_contents decls 
+  in
   close_section false process_segment s
 
 let save_module_to s f =