Mise a jour des dependances

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2249 85f007b7-540e-0410-9357-904b9bb8a0f7
author: clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> 2001-11-29 13:38:18 +0000
committer: clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> 2001-11-29 13:38:18 +0000
commit: 28d905bd62786e0938cd333ddcdc2f7754dd0165 (patch)
tree: 3ec3990196d8e80c59d0b595dbac61c3adf63100
parent: 476d1f90525a97f18fa1c2adbde453f5e1e9213c (diff)
8 files changed, 539 insertions, 519 deletions
diff --git a/.depend b/.depend
index 3f6a7b46b..038ea4799 100644
--- a/.depend
+++ b/.depend
@@ -1,5 +1,6 @@
 kernel/closure.cmi: kernel/environ.cmi kernel/esubst.cmi kernel/names.cmi \
     lib/pp.cmi kernel/term.cmi 
+kernel/conv_oracle.cmi: kernel/closure.cmi kernel/names.cmi 
 kernel/cooking.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/declarations.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
@@ -11,7 +12,7 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi 
 kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi kernel/type_errors.cmi kernel/univ.cmi 
-kernel/names.cmi: lib/pp.cmi lib/predicate.cmi 
+kernel/names.cmi: lib/predicate.cmi 
 kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
 kernel/safe_typing.cmi: kernel/cooking.cmi kernel/declarations.cmi \
@@ -24,8 +25,6 @@ kernel/typeops.cmi: kernel/environ.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/indtypes.cmi library/libobject.cmi \
     library/library.cmi kernel/names.cmi library/nametab.cmi \
@@ -41,12 +40,13 @@ library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi
 library/libobject.cmi: kernel/names.cmi 
 library/library.cmi: library/lib.cmi library/libobject.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi lib/system.cmi 
-library/nameops.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi 
+library/nameops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/term.cmi 
 library/nametab.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     lib/util.cmi 
-library/opaque.cmi: kernel/closure.cmi kernel/environ.cmi kernel/names.cmi \
-    kernel/safe_typing.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 pretyping/evd.cmi \
@@ -83,7 +83,7 @@ pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi pretyping/inductiveops.cmi kernel/names.cmi \
     pretyping/rawterm.cmi kernel/term.cmi 
 pretyping/cbv.cmi: kernel/closure.cmi kernel/environ.cmi kernel/esubst.cmi \
-    pretyping/evd.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi 
+    kernel/names.cmi kernel/term.cmi 
 pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/libobject.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi kernel/term.cmi 
@@ -224,18 +224,18 @@ toplevel/recordobj.cmi: library/nametab.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/environ.cmi pretyping/evd.cmi \
     kernel/names.cmi kernel/term.cmi toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     library/nametab.cmi proofs/proof_type.cmi 
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \
     contrib/correctness/ptype.cmi kernel/term.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 
@@ -332,6 +332,10 @@ kernel/closure.cmo: kernel/environ.cmi kernel/esubst.cmi kernel/names.cmi \
 kernel/closure.cmx: kernel/environ.cmx kernel/esubst.cmx kernel/names.cmx \
     lib/pp.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
     kernel/closure.cmi 
+kernel/conv_oracle.cmo: kernel/closure.cmi kernel/names.cmi \
+    kernel/conv_oracle.cmi 
+kernel/conv_oracle.cmx: kernel/closure.cmx kernel/names.cmx \
+    kernel/conv_oracle.cmi 
 kernel/cooking.cmo: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
     kernel/term.cmi lib/util.cmi kernel/cooking.cmi 
@@ -366,12 +370,14 @@ kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \
     kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \
     kernel/names.cmi 
-kernel/reduction.cmo: kernel/closure.cmi kernel/declarations.cmi \
-    kernel/environ.cmi kernel/esubst.cmi kernel/names.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/reduction.cmi 
-kernel/reduction.cmx: kernel/closure.cmx kernel/declarations.cmx \
-    kernel/environ.cmx kernel/esubst.cmx kernel/names.cmx kernel/sign.cmx \
-    kernel/term.cmx kernel/univ.cmx lib/util.cmx kernel/reduction.cmi 
+kernel/reduction.cmo: kernel/closure.cmi kernel/conv_oracle.cmi \
+    kernel/declarations.cmi kernel/environ.cmi kernel/esubst.cmi \
+    kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \
+    lib/util.cmi kernel/reduction.cmi 
+kernel/reduction.cmx: kernel/closure.cmx kernel/conv_oracle.cmx \
+    kernel/declarations.cmx kernel/environ.cmx kernel/esubst.cmx \
+    kernel/names.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \
+    lib/util.cmx kernel/reduction.cmi 
 kernel/safe_typing.cmo: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/indtypes.cmi kernel/inductive.cmi \
     kernel/names.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
@@ -418,32 +424,24 @@ 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 
 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.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/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: kernel/declarations.cmi kernel/environ.cmi \
     library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
     kernel/inductive.cmi library/lib.cmi library/libobject.cmi \
@@ -501,23 +499,17 @@ library/library.cmx: kernel/environ.cmx library/global.cmx library/lib.cmx \
     library/nametab.cmx lib/options.cmx lib/pp.cmx library/summary.cmx \
     lib/system.cmx lib/util.cmx library/library.cmi 
 library/nameops.cmo: kernel/declarations.cmi kernel/environ.cmi \
-    kernel/names.cmi kernel/term.cmi lib/util.cmi library/nameops.cmi 
+    kernel/names.cmi lib/pp.cmi kernel/term.cmi lib/util.cmi \
+    library/nameops.cmi 
 library/nameops.cmx: kernel/declarations.cmx kernel/environ.cmx \
-    kernel/names.cmx kernel/term.cmx lib/util.cmx library/nameops.cmi 
+    kernel/names.cmx lib/pp.cmx kernel/term.cmx lib/util.cmx \
+    library/nameops.cmi 
 library/nametab.cmo: kernel/declarations.cmi kernel/environ.cmi \
     library/nameops.cmi kernel/names.cmi lib/pp.cmi library/summary.cmi \
     lib/util.cmi library/nametab.cmi 
 library/nametab.cmx: kernel/declarations.cmx kernel/environ.cmx \
     library/nameops.cmx kernel/names.cmx lib/pp.cmx library/summary.cmx \
     lib/util.cmx library/nametab.cmi 
-library/opaque.cmo: kernel/closure.cmi kernel/declarations.cmi \
-    kernel/environ.cmi library/global.cmi kernel/names.cmi \
-    library/nametab.cmi lib/pp.cmi library/summary.cmi kernel/term.cmi \
-    lib/util.cmi library/opaque.cmi 
-library/opaque.cmx: kernel/closure.cmx kernel/declarations.cmx \
-    kernel/environ.cmx library/global.cmx kernel/names.cmx \
-    library/nametab.cmx lib/pp.cmx library/summary.cmx kernel/term.cmx \
-    lib/util.cmx library/opaque.cmi 
 library/states.cmo: library/lib.cmi library/library.cmi library/summary.cmi \
     lib/system.cmi library/states.cmi 
 library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
@@ -526,6 +518,14 @@ 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: 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/ast.cmo: parsing/coqast.cmi lib/dyn.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 kernel/names.cmx \
@@ -646,16 +646,16 @@ parsing/prettyp.cmx: pretyping/classops.cmx kernel/declarations.cmx \
     kernel/term.cmx pretyping/termops.cmx lib/util.cmx parsing/prettyp.cmi 
 parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
     lib/dyn.cmi kernel/environ.cmi parsing/esyntax.cmi parsing/extend.cmi \
-    library/global.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
-    pretyping/pattern.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \
-    parsing/termast.cmi pretyping/termops.cmi lib/util.cmi \
-    parsing/printer.cmi 
+    library/global.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \
+    kernel/sign.cmi kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \
+    lib/util.cmi parsing/printer.cmi 
 parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
     lib/dyn.cmx kernel/environ.cmx parsing/esyntax.cmx parsing/extend.cmx \
-    library/global.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
-    pretyping/pattern.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \
-    parsing/termast.cmx pretyping/termops.cmx lib/util.cmx \
-    parsing/printer.cmi 
+    library/global.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \
+    kernel/sign.cmx kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \
+    lib/util.cmx parsing/printer.cmi 
 parsing/q_coqast.cmo: parsing/coqast.cmi kernel/names.cmi parsing/pcoq.cmi 
 parsing/q_coqast.cmx: parsing/coqast.cmx kernel/names.cmx parsing/pcoq.cmx 
 parsing/search.cmo: parsing/astterm.cmi parsing/coqast.cmi parsing/coqlib.cmi \
@@ -704,14 +704,12 @@ pretyping/cases.cmx: pretyping/coercion.cmx kernel/declarations.cmx \
     pretyping/reductionops.cmx pretyping/retyping.cmx kernel/sign.cmx \
     kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx \
     kernel/typeops.cmx lib/util.cmx pretyping/cases.cmi 
-pretyping/cbv.cmo: kernel/closure.cmi kernel/declarations.cmi \
-    kernel/environ.cmi kernel/esubst.cmi pretyping/evd.cmi \
-    pretyping/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
-    kernel/univ.cmi lib/util.cmi pretyping/cbv.cmi 
-pretyping/cbv.cmx: kernel/closure.cmx kernel/declarations.cmx \
-    kernel/environ.cmx kernel/esubst.cmx pretyping/evd.cmx \
-    pretyping/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
-    kernel/univ.cmx lib/util.cmx pretyping/cbv.cmi 
+pretyping/cbv.cmo: kernel/closure.cmi kernel/environ.cmi kernel/esubst.cmi \
+    pretyping/evd.cmi pretyping/instantiate.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/term.cmi kernel/univ.cmi lib/util.cmi pretyping/cbv.cmi 
+pretyping/cbv.cmx: kernel/closure.cmx kernel/environ.cmx kernel/esubst.cmx \
+    pretyping/evd.cmx pretyping/instantiate.cmx kernel/names.cmx lib/pp.cmx \
+    kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/cbv.cmi 
 pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \
     library/global.cmi library/lib.cmi library/libobject.cmi \
     library/library.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
@@ -886,16 +884,20 @@ pretyping/syntax_def.cmx: library/lib.cmx library/libobject.cmx \
     library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
     pretyping/rawterm.cmx library/summary.cmx lib/util.cmx \
     pretyping/syntax_def.cmi 
-pretyping/tacred.cmo: pretyping/cbv.cmi kernel/closure.cmi kernel/environ.cmi \
-    pretyping/evd.cmi kernel/inductive.cmi pretyping/instantiate.cmi \
-    library/nameops.cmi kernel/names.cmi library/opaque.cmi lib/pp.cmi \
-    pretyping/reductionops.cmi library/summary.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi pretyping/tacred.cmi 
-pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx kernel/environ.cmx \
-    pretyping/evd.cmx kernel/inductive.cmx pretyping/instantiate.cmx \
-    library/nameops.cmx kernel/names.cmx library/opaque.cmx lib/pp.cmx \
-    pretyping/reductionops.cmx library/summary.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx pretyping/tacred.cmi 
+pretyping/tacred.cmo: pretyping/cbv.cmi kernel/closure.cmi \
+    kernel/conv_oracle.cmi kernel/declarations.cmi kernel/environ.cmi \
+    pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \
+    pretyping/instantiate.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi pretyping/reductionops.cmi \
+    library/summary.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
+    pretyping/tacred.cmi 
+pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx \
+    kernel/conv_oracle.cmx kernel/declarations.cmx kernel/environ.cmx \
+    pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \
+    pretyping/instantiate.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx pretyping/reductionops.cmx \
+    library/summary.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
+    pretyping/tacred.cmi 
 pretyping/termops.cmo: kernel/environ.cmi library/global.cmi \
     library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
@@ -914,17 +916,17 @@ pretyping/typing.cmx: kernel/environ.cmx kernel/inductive.cmx \
     kernel/typeops.cmx lib/util.cmx pretyping/typing.cmi 
 proofs/clenv.cmo: kernel/environ.cmi proofs/evar_refiner.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi pretyping/instantiate.cmi \
-    proofs/logic.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
-    proofs/refiner.cmi pretyping/retyping.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \
+    proofs/logic.cmi library/nameops.cmi kernel/names.cmi lib/pp.cmi \
+    parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    pretyping/reductionops.cmi proofs/refiner.cmi pretyping/retyping.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \
     pretyping/typing.cmi lib/util.cmi proofs/clenv.cmi 
 proofs/clenv.cmx: kernel/environ.cmx proofs/evar_refiner.cmx \
     pretyping/evarutil.cmx pretyping/evd.cmx pretyping/instantiate.cmx \
-    proofs/logic.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \
-    proofs/refiner.cmx pretyping/retyping.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
+    proofs/logic.cmx library/nameops.cmx kernel/names.cmx lib/pp.cmx \
+    parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
+    pretyping/reductionops.cmx proofs/refiner.cmx pretyping/retyping.cmx \
+    kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
     pretyping/typing.cmx lib/util.cmx proofs/clenv.cmi 
 proofs/evar_refiner.cmo: parsing/astterm.cmi kernel/environ.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
@@ -942,44 +944,46 @@ proofs/evar_refiner.cmx: parsing/astterm.cmx kernel/environ.cmx \
     proofs/evar_refiner.cmi 
 proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
-    kernel/inductive.cmi pretyping/inductiveops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
-    kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \
-    kernel/type_errors.cmi kernel/typeops.cmi pretyping/typing.cmi \
-    lib/util.cmi proofs/logic.cmi 
+    kernel/inductive.cmi pretyping/inductiveops.cmi library/nameops.cmi \
+    kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
+    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
+    pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \
+    pretyping/termops.cmi kernel/type_errors.cmi kernel/typeops.cmi \
+    pretyping/typing.cmi lib/util.cmi proofs/logic.cmi 
 proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
     pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \
-    kernel/inductive.cmx pretyping/inductiveops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
-    kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
-    kernel/type_errors.cmx kernel/typeops.cmx pretyping/typing.cmx \
-    lib/util.cmx proofs/logic.cmi 
+    kernel/inductive.cmx pretyping/inductiveops.cmx library/nameops.cmx \
+    kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
+    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \
+    pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
+    pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \
+    pretyping/typing.cmx lib/util.cmx proofs/logic.cmi 
 proofs/pfedit.cmo: parsing/astterm.cmi kernel/declarations.cmi \
     library/declare.cmi lib/edit.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi pretyping/evd.cmi library/lib.cmi \
-    kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
-    kernel/safe_typing.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
-    pretyping/typing.cmi lib/util.cmi proofs/pfedit.cmi 
+    library/nameops.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    proofs/proof_type.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+    proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
+    proofs/pfedit.cmi 
 proofs/pfedit.cmx: parsing/astterm.cmx kernel/declarations.cmx \
     library/declare.cmx lib/edit.cmx kernel/environ.cmx \
     proofs/evar_refiner.cmx pretyping/evd.cmx library/lib.cmx \
-    kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
-    kernel/safe_typing.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
-    pretyping/typing.cmx lib/util.cmx proofs/pfedit.cmi 
+    library/nameops.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \
+    proofs/proof_type.cmx kernel/safe_typing.cmx kernel/sign.cmx \
+    proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
+    proofs/pfedit.cmi 
 proofs/proof_trees.cmo: parsing/ast.cmi kernel/closure.cmi \
     pretyping/detyping.cmi kernel/environ.cmi pretyping/evarutil.cmi \
-    pretyping/evd.cmi library/global.cmi kernel/names.cmi library/nametab.cmi \
-    lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi kernel/sign.cmi \
-    pretyping/tacred.cmi kernel/term.cmi parsing/termast.cmi \
+    pretyping/evd.cmi library/global.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \
+    kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi parsing/termast.cmi \
     pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
     proofs/proof_trees.cmi 
 proofs/proof_trees.cmx: parsing/ast.cmx kernel/closure.cmx \
     pretyping/detyping.cmx kernel/environ.cmx pretyping/evarutil.cmx \
-    pretyping/evd.cmx library/global.cmx kernel/names.cmx library/nametab.cmx \
-    lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx kernel/sign.cmx \
-    pretyping/tacred.cmx kernel/term.cmx parsing/termast.cmx \
+    pretyping/evd.cmx library/global.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \
+    kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx parsing/termast.cmx \
     pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
     proofs/proof_trees.cmi 
 proofs/proof_type.cmo: parsing/coqast.cmi kernel/environ.cmi \
@@ -1003,10 +1007,10 @@ proofs/refiner.cmx: parsing/ast.cmx kernel/environ.cmx pretyping/evarutil.cmx \
     kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \
     proofs/refiner.cmi 
 proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \
-    parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \
-    lib/dyn.cmi kernel/environ.cmi pretyping/evd.cmi library/global.cmi \
-    lib/gmap.cmi library/lib.cmi library/libobject.cmi library/nameops.cmi \
-    kernel/names.cmi library/nametab.cmi library/opaque.cmi lib/options.cmi \
+    kernel/conv_oracle.cmi parsing/coqast.cmi kernel/declarations.cmi \
+    library/declare.cmi lib/dyn.cmi kernel/environ.cmi pretyping/evd.cmi \
+    library/global.cmi lib/gmap.cmi library/lib.cmi library/libobject.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
     pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi \
     pretyping/pretyping.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
     kernel/safe_typing.cmi kernel/sign.cmi library/summary.cmi \
@@ -1014,10 +1018,10 @@ proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \
     kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
     proofs/tacinterp.cmi 
 proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \
-    parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \
-    lib/dyn.cmx kernel/environ.cmx pretyping/evd.cmx library/global.cmx \
-    lib/gmap.cmx library/lib.cmx library/libobject.cmx library/nameops.cmx \
-    kernel/names.cmx library/nametab.cmx library/opaque.cmx lib/options.cmx \
+    kernel/conv_oracle.cmx parsing/coqast.cmx kernel/declarations.cmx \
+    library/declare.cmx lib/dyn.cmx kernel/environ.cmx pretyping/evd.cmx \
+    library/global.cmx lib/gmap.cmx library/lib.cmx library/libobject.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
     pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx \
     pretyping/pretyping.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
     kernel/safe_typing.cmx kernel/sign.cmx library/summary.cmx \
@@ -1027,17 +1031,17 @@ proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \
 proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi library/declare.cmi \
     kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
     library/global.cmi pretyping/instantiate.cmi proofs/logic.cmi \
-    kernel/names.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi pretyping/reductionops.cmi proofs/refiner.cmi \
-    kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi \
+    library/nameops.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
+    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
+    proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi \
     pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
     proofs/tacmach.cmi 
 proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx library/declare.cmx \
     kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \
     library/global.cmx pretyping/instantiate.cmx proofs/logic.cmx \
-    kernel/names.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx pretyping/reductionops.cmx proofs/refiner.cmx \
-    kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx \
+    library/nameops.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
+    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \
+    proofs/refiner.cmx kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx \
     pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
     proofs/tacmach.cmi 
 proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \
@@ -1113,15 +1117,15 @@ tactics/dhyp.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
 tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi 
 tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi 
 tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi proofs/evar_refiner.cmi \
-    lib/explore.cmi proofs/logic.cmi kernel/names.cmi pretyping/pattern.cmi \
-    lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
-    kernel/reduction.cmi parsing/search.cmi kernel/sign.cmi \
+    lib/explore.cmi proofs/logic.cmi library/nameops.cmi kernel/names.cmi \
+    pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \
     proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
     kernel/term.cmi pretyping/termops.cmi lib/util.cmi 
 tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx proofs/evar_refiner.cmx \
-    lib/explore.cmx proofs/logic.cmx kernel/names.cmx pretyping/pattern.cmx \
-    lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
-    kernel/reduction.cmx parsing/search.cmx kernel/sign.cmx \
+    lib/explore.cmx proofs/logic.cmx library/nameops.cmx kernel/names.cmx \
+    pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
+    proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx pretyping/termops.cmx lib/util.cmx 
 tactics/elim.cmo: proofs/clenv.cmi library/declare.cmi kernel/environ.cmi \
@@ -1154,8 +1158,9 @@ tactics/equality.cmo: parsing/astterm.cmi proofs/clenv.cmi parsing/coqast.cmi \
     library/global.cmi lib/gmapl.cmi tactics/hipattern.cmi \
     pretyping/indrec.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \
     pretyping/instantiate.cmi library/lib.cmi library/libobject.cmi \
-    proofs/logic.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
-    proofs/proof_type.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
+    proofs/logic.cmi library/nameops.cmi kernel/names.cmi \
+    pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \
+    pretyping/reductionops.cmi pretyping/retyping.cmi \
     tactics/setoid_replace.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
     pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \
     kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi \
@@ -1167,8 +1172,9 @@ tactics/equality.cmx: parsing/astterm.cmx proofs/clenv.cmx parsing/coqast.cmx \
     library/global.cmx lib/gmapl.cmx tactics/hipattern.cmx \
     pretyping/indrec.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \
     pretyping/instantiate.cmx library/lib.cmx library/libobject.cmx \
-    proofs/logic.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
-    proofs/proof_type.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
+    proofs/logic.cmx library/nameops.cmx kernel/names.cmx \
+    pretyping/pattern.cmx lib/pp.cmx proofs/proof_type.cmx \
+    pretyping/reductionops.cmx pretyping/retyping.cmx \
     tactics/setoid_replace.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
     pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \
@@ -1193,19 +1199,21 @@ tactics/hipattern.cmx: proofs/clenv.cmx parsing/coqlib.cmx \
 tactics/inv.cmo: tactics/auto.cmi proofs/clenv.cmi parsing/coqlib.cmi \
     tactics/elim.cmi kernel/environ.cmi tactics/equality.cmi \
     proofs/evar_refiner.cmi library/global.cmi pretyping/inductiveops.cmi \
-    kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_type.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \
-    pretyping/typing.cmi lib/util.cmi tactics/wcclausenv.cmi tactics/inv.cmi 
+    library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
+    parsing/printer.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
+    pretyping/retyping.cmi kernel/sign.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+    pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
+    tactics/wcclausenv.cmi tactics/inv.cmi 
 tactics/inv.cmx: tactics/auto.cmx proofs/clenv.cmx parsing/coqlib.cmx \
     tactics/elim.cmx kernel/environ.cmx tactics/equality.cmx \
     proofs/evar_refiner.cmx library/global.cmx pretyping/inductiveops.cmx \
-    kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_type.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
-    kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \
-    pretyping/typing.cmx lib/util.cmx tactics/wcclausenv.cmx tactics/inv.cmi 
+    library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
+    parsing/printer.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \
+    pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+    pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
+    tactics/wcclausenv.cmx tactics/inv.cmi 
 tactics/leminv.cmo: parsing/astterm.cmi proofs/clenv.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \
@@ -1334,12 +1342,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
     proofs/proof_trees.cmx pretyping/reductionops.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/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/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/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \
@@ -1436,16 +1444,18 @@ toplevel/fhimsg.cmx: kernel/environ.cmx parsing/g_minicoq.cmx \
     kernel/term.cmx kernel/type_errors.cmx lib/util.cmx toplevel/fhimsg.cmi 
 toplevel/himsg.cmo: parsing/ast.cmi pretyping/cases.cmi kernel/environ.cmi \
     library/global.cmi kernel/indtypes.cmi kernel/inductive.cmi \
-    proofs/logic.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
-    pretyping/pretype_errors.cmi parsing/printer.cmi kernel/reduction.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \
-    kernel/type_errors.cmi lib/util.cmi toplevel/himsg.cmi 
+    proofs/logic.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \
+    lib/pp.cmi pretyping/pretype_errors.cmi parsing/printer.cmi \
+    kernel/reduction.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
+    pretyping/termops.cmi kernel/type_errors.cmi lib/util.cmi \
+    toplevel/himsg.cmi 
 toplevel/himsg.cmx: parsing/ast.cmx pretyping/cases.cmx kernel/environ.cmx \
     library/global.cmx kernel/indtypes.cmx kernel/inductive.cmx \
-    proofs/logic.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
-    pretyping/pretype_errors.cmx parsing/printer.cmx kernel/reduction.cmx \
-    kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
-    kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi 
+    proofs/logic.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \
+    lib/pp.cmx pretyping/pretype_errors.cmx parsing/printer.cmx \
+    kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
+    pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \
+    toplevel/himsg.cmi 
 toplevel/line_oriented_parser.cmo: toplevel/line_oriented_parser.cmi 
 toplevel/line_oriented_parser.cmx: toplevel/line_oriented_parser.cmi 
 toplevel/metasyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
@@ -1484,29 +1494,29 @@ toplevel/record.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \
     toplevel/command.cmi parsing/coqast.cmi kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
     library/global.cmi kernel/indtypes.cmi kernel/inductive.cmi \
-    pretyping/inductiveops.cmi kernel/names.cmi library/nametab.cmi \
-    lib/options.cmi lib/pp.cmi parsing/printer.cmi pretyping/recordops.cmi \
-    kernel/safe_typing.cmi kernel/term.cmi pretyping/termops.cmi \
-    kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
-    toplevel/record.cmi 
+    pretyping/inductiveops.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \
+    pretyping/recordops.cmi kernel/safe_typing.cmi kernel/term.cmi \
+    pretyping/termops.cmi kernel/type_errors.cmi kernel/typeops.cmi \
+    lib/util.cmi toplevel/record.cmi 
 toplevel/record.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \
     toplevel/command.cmx parsing/coqast.cmx kernel/declarations.cmx \
     library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \
     library/global.cmx kernel/indtypes.cmx kernel/inductive.cmx \
-    pretyping/inductiveops.cmx kernel/names.cmx library/nametab.cmx \
-    lib/options.cmx lib/pp.cmx parsing/printer.cmx pretyping/recordops.cmx \
-    kernel/safe_typing.cmx kernel/term.cmx pretyping/termops.cmx \
-    kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
-    toplevel/record.cmi 
+    pretyping/inductiveops.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/options.cmx lib/pp.cmx parsing/printer.cmx \
+    pretyping/recordops.cmx kernel/safe_typing.cmx kernel/term.cmx \
+    pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \
+    lib/util.cmx toplevel/record.cmi 
 toplevel/recordobj.cmo: pretyping/classops.cmi library/declare.cmi \
     kernel/environ.cmi library/global.cmi pretyping/instantiate.cmi \
-    library/lib.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    pretyping/recordops.cmi kernel/term.cmi pretyping/termops.cmi \
+    library/lib.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \
+    lib/pp.cmi pretyping/recordops.cmi kernel/term.cmi pretyping/termops.cmi \
     lib/util.cmi toplevel/recordobj.cmi 
 toplevel/recordobj.cmx: pretyping/classops.cmx library/declare.cmx \
     kernel/environ.cmx library/global.cmx pretyping/instantiate.cmx \
-    library/lib.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    pretyping/recordops.cmx kernel/term.cmx pretyping/termops.cmx \
+    library/lib.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \
+    lib/pp.cmx pretyping/recordops.cmx kernel/term.cmx pretyping/termops.cmx \
     lib/util.cmx toplevel/recordobj.cmi 
 toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi library/lib.cmi \
     toplevel/mltop.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
@@ -1518,16 +1528,6 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx library/lib.cmx \
     toplevel/vernac.cmx toplevel/vernacinterp.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: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
-    library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \
-    parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \
-    pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
-    library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \
-    parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \
-    pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \
     parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \
@@ -1536,16 +1536,15 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     library/global.cmi library/goptions.cmi library/impargs.cmi \
     pretyping/inductiveops.cmi library/lib.cmi library/library.cmi \
     toplevel/metasyntax.cmi toplevel/mltop.cmi library/nameops.cmi \
-    kernel/names.cmi library/nametab.cmi library/opaque.cmi lib/options.cmi \
-    proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/prettyp.cmi \
-    parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
-    toplevel/record.cmi toplevel/recordobj.cmi proofs/refiner.cmi \
-    kernel/safe_typing.cmi parsing/search.cmi library/states.cmi \
-    pretyping/syntax_def.cmi lib/system.cmi proofs/tacinterp.cmi \
-    proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \
-    tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi \
-    pretyping/termops.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
+    kernel/names.cmi library/nametab.cmi lib/options.cmi proofs/pfedit.cmi \
+    lib/pp.cmi lib/pp_control.cmi parsing/prettyp.cmi parsing/printer.cmi \
+    proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \
+    toplevel/recordobj.cmi proofs/refiner.cmi kernel/safe_typing.cmi \
+    parsing/search.cmi library/states.cmi pretyping/syntax_def.cmi \
+    lib/system.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
+    pretyping/tacred.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \
+    kernel/term.cmi parsing/termast.cmi kernel/typeops.cmi kernel/univ.cmi \
+    lib/util.cmi toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
     toplevel/class.cmx pretyping/classops.cmx toplevel/command.cmx \
     parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \
@@ -1554,16 +1553,15 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
     library/global.cmx library/goptions.cmx library/impargs.cmx \
     pretyping/inductiveops.cmx library/lib.cmx library/library.cmx \
     toplevel/metasyntax.cmx toplevel/mltop.cmx library/nameops.cmx \
-    kernel/names.cmx library/nametab.cmx library/opaque.cmx lib/options.cmx \
-    proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx parsing/prettyp.cmx \
-    parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
-    toplevel/record.cmx toplevel/recordobj.cmx proofs/refiner.cmx \
-    kernel/safe_typing.cmx parsing/search.cmx library/states.cmx \
-    pretyping/syntax_def.cmx lib/system.cmx proofs/tacinterp.cmx \
-    proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \
-    tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \
-    pretyping/termops.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
+    kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pfedit.cmx \
+    lib/pp.cmx lib/pp_control.cmx parsing/prettyp.cmx parsing/printer.cmx \
+    proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \
+    toplevel/recordobj.cmx proofs/refiner.cmx kernel/safe_typing.cmx \
+    parsing/search.cmx library/states.cmx pretyping/syntax_def.cmx \
+    lib/system.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
+    pretyping/tacred.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \
+    kernel/term.cmx parsing/termast.cmx kernel/typeops.cmx kernel/univ.cmx \
+    lib/util.cmx toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
 toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi \
     toplevel/command.cmi parsing/coqast.cmi lib/dyn.cmi toplevel/himsg.cmi \
     kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
@@ -1574,18 +1572,16 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
     proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \
     toplevel/vernacinterp.cmi 
-contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \
-    library/declare.cmi pretyping/detyping.cmi kernel/indtypes.cmi \
-    kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
-    contrib/correctness/pmisc.cmi pretyping/rawterm.cmi toplevel/record.cmi \
-    kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi \
-    lib/util.cmi contrib/correctness/pcic.cmi 
-contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \
-    library/declare.cmx pretyping/detyping.cmx kernel/indtypes.cmx \
-    kernel/names.cmx library/nametab.cmx contrib/correctness/past.cmi \
-    contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \
-    kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \
-    lib/util.cmx contrib/correctness/pcic.cmi 
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
+    library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \
+    parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \
+    pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+    toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
+    library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \
+    parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \
+    pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+    toplevel/vernac.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 \
@@ -1598,6 +1594,18 @@ contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.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: parsing/ast.cmi kernel/declarations.cmi \
+    library/declare.cmi pretyping/detyping.cmi kernel/indtypes.cmi \
+    kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
+    contrib/correctness/pmisc.cmi pretyping/rawterm.cmi toplevel/record.cmi \
+    kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi \
+    lib/util.cmi contrib/correctness/pcic.cmi 
+contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \
+    library/declare.cmx pretyping/detyping.cmx kernel/indtypes.cmx \
+    kernel/names.cmx library/nametab.cmx contrib/correctness/past.cmi \
+    contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \
+    kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \
+    lib/util.cmx contrib/correctness/pcic.cmi 
 contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \
     kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
     contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -1608,34 +1616,36 @@ contrib/correctness/pdb.cmx: library/declare.cmx library/global.cmx \
     contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
     contrib/correctness/perror.cmx contrib/correctness/ptype.cmi \
     kernel/term.cmx pretyping/termops.cmx contrib/correctness/pdb.cmi 
-contrib/correctness/peffect.cmo: toplevel/himsg.cmi kernel/names.cmi \
-    contrib/correctness/pmisc.cmi lib/pp.cmi lib/util.cmi \
+contrib/correctness/peffect.cmo: toplevel/himsg.cmi library/nameops.cmi \
+    kernel/names.cmi contrib/correctness/pmisc.cmi lib/pp.cmi lib/util.cmi \
     contrib/correctness/peffect.cmi 
-contrib/correctness/peffect.cmx: toplevel/himsg.cmx kernel/names.cmx \
-    contrib/correctness/pmisc.cmx lib/pp.cmx lib/util.cmx \
+contrib/correctness/peffect.cmx: toplevel/himsg.cmx library/nameops.cmx \
+    kernel/names.cmx contrib/correctness/pmisc.cmx lib/pp.cmx lib/util.cmx \
     contrib/correctness/peffect.cmi 
 contrib/correctness/penv.cmo: toplevel/himsg.cmi library/lib.cmi \
-    library/libobject.cmi library/library.cmi kernel/names.cmi \
-    lib/options.cmi contrib/correctness/past.cmi \
+    library/libobject.cmi library/library.cmi library/nameops.cmi \
+    kernel/names.cmi lib/options.cmi contrib/correctness/past.cmi \
     contrib/correctness/perror.cmi contrib/correctness/pmisc.cmi lib/pp.cmi \
     contrib/correctness/ptype.cmi library/summary.cmi kernel/term.cmi \
     contrib/correctness/penv.cmi 
 contrib/correctness/penv.cmx: toplevel/himsg.cmx library/lib.cmx \
-    library/libobject.cmx library/library.cmx kernel/names.cmx \
-    lib/options.cmx contrib/correctness/past.cmi \
+    library/libobject.cmx library/library.cmx library/nameops.cmx \
+    kernel/names.cmx lib/options.cmx contrib/correctness/past.cmi \
     contrib/correctness/perror.cmx contrib/correctness/pmisc.cmx lib/pp.cmx \
     contrib/correctness/ptype.cmi library/summary.cmx kernel/term.cmx \
     contrib/correctness/penv.cmi 
 contrib/correctness/perror.cmo: library/declare.cmi pretyping/evd.cmi \
-    library/global.cmi toplevel/himsg.cmi kernel/names.cmi \
-    contrib/correctness/past.cmi contrib/correctness/peffect.cmi lib/pp.cmi \
-    contrib/correctness/ptype.cmi pretyping/reductionops.cmi kernel/term.cmi \
-    lib/util.cmi contrib/correctness/perror.cmi 
+    library/global.cmi toplevel/himsg.cmi library/nameops.cmi \
+    kernel/names.cmi contrib/correctness/past.cmi \
+    contrib/correctness/peffect.cmi lib/pp.cmi contrib/correctness/ptype.cmi \
+    pretyping/reductionops.cmi kernel/term.cmi lib/util.cmi \
+    contrib/correctness/perror.cmi 
 contrib/correctness/perror.cmx: library/declare.cmx pretyping/evd.cmx \
-    library/global.cmx toplevel/himsg.cmx kernel/names.cmx \
-    contrib/correctness/past.cmi contrib/correctness/peffect.cmx lib/pp.cmx \
-    contrib/correctness/ptype.cmi pretyping/reductionops.cmx kernel/term.cmx \
-    lib/util.cmx contrib/correctness/perror.cmi 
+    library/global.cmx toplevel/himsg.cmx library/nameops.cmx \
+    kernel/names.cmx contrib/correctness/past.cmi \
+    contrib/correctness/peffect.cmx lib/pp.cmx contrib/correctness/ptype.cmi \
+    pretyping/reductionops.cmx kernel/term.cmx lib/util.cmx \
+    contrib/correctness/perror.cmi 
 contrib/correctness/pextract.cmo: parsing/ast.cmi pretyping/evd.cmi \
     toplevel/himsg.cmi library/library.cmi kernel/names.cmi \
     library/nametab.cmi contrib/extraction/ocaml.cmi \
@@ -1696,39 +1706,39 @@ contrib/correctness/pred.cmo: pretyping/evd.cmi library/global.cmi \
 contrib/correctness/pred.cmx: pretyping/evd.cmx library/global.cmx \
     contrib/correctness/past.cmi contrib/correctness/pmisc.cmx lib/pp.cmx \
     pretyping/reductionops.cmx kernel/term.cmx contrib/correctness/pred.cmi 
-contrib/correctness/prename.cmo: toplevel/himsg.cmi kernel/names.cmi \
-    contrib/correctness/pmisc.cmi lib/pp.cmi lib/util.cmi \
+contrib/correctness/prename.cmo: toplevel/himsg.cmi library/nameops.cmi \
+    kernel/names.cmi contrib/correctness/pmisc.cmi lib/pp.cmi lib/util.cmi \
     contrib/correctness/prename.cmi 
-contrib/correctness/prename.cmx: toplevel/himsg.cmx kernel/names.cmx \
-    contrib/correctness/pmisc.cmx lib/pp.cmx lib/util.cmx \
+contrib/correctness/prename.cmx: toplevel/himsg.cmx library/nameops.cmx \
+    kernel/names.cmx contrib/correctness/pmisc.cmx lib/pp.cmx lib/util.cmx \
     contrib/correctness/prename.cmi 
 contrib/correctness/psyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
     parsing/coqast.cmi library/declare.cmi lib/dyn.cmi pretyping/evd.cmi \
     parsing/g_zsyntax.cmi library/global.cmi toplevel/himsg.cmi \
-    kernel/names.cmi lib/options.cmi contrib/correctness/past.cmi \
-    contrib/correctness/pcicenv.cmi parsing/pcoq.cmi \
-    contrib/correctness/pdb.cmi contrib/correctness/peffect.cmi \
-    contrib/correctness/penv.cmi contrib/correctness/pmisc.cmi \
-    contrib/correctness/pmonad.cmi lib/pp.cmi contrib/correctness/prename.cmi \
-    contrib/correctness/ptactic.cmi contrib/correctness/ptype.cmi \
-    contrib/correctness/ptyping.cmi contrib/correctness/putil.cmi \
-    kernel/reduction.cmi kernel/safe_typing.cmi proofs/tacinterp.cmi \
-    kernel/term.cmi parsing/termast.cmi lib/util.cmi toplevel/vernac.cmi \
-    toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \
+    library/nameops.cmi kernel/names.cmi lib/options.cmi \
+    contrib/correctness/past.cmi contrib/correctness/pcicenv.cmi \
+    parsing/pcoq.cmi contrib/correctness/pdb.cmi \
+    contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi lib/pp.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptactic.cmi \
+    contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmi \
+    contrib/correctness/putil.cmi kernel/reduction.cmi kernel/safe_typing.cmi \
+    proofs/tacinterp.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \
+    toplevel/vernac.cmi toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \
     contrib/correctness/psyntax.cmi 
 contrib/correctness/psyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
     parsing/coqast.cmx library/declare.cmx lib/dyn.cmx pretyping/evd.cmx \
     parsing/g_zsyntax.cmx library/global.cmx toplevel/himsg.cmx \
-    kernel/names.cmx lib/options.cmx contrib/correctness/past.cmi \
-    contrib/correctness/pcicenv.cmx parsing/pcoq.cmx \
-    contrib/correctness/pdb.cmx contrib/correctness/peffect.cmx \
-    contrib/correctness/penv.cmx contrib/correctness/pmisc.cmx \
-    contrib/correctness/pmonad.cmx lib/pp.cmx contrib/correctness/prename.cmx \
-    contrib/correctness/ptactic.cmx contrib/correctness/ptype.cmi \
-    contrib/correctness/ptyping.cmx contrib/correctness/putil.cmx \
-    kernel/reduction.cmx kernel/safe_typing.cmx proofs/tacinterp.cmx \
-    kernel/term.cmx parsing/termast.cmx lib/util.cmx toplevel/vernac.cmx \
-    toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \
+    library/nameops.cmx kernel/names.cmx lib/options.cmx \
+    contrib/correctness/past.cmi contrib/correctness/pcicenv.cmx \
+    parsing/pcoq.cmx contrib/correctness/pdb.cmx \
+    contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx lib/pp.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptactic.cmx \
+    contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmx \
+    contrib/correctness/putil.cmx kernel/reduction.cmx kernel/safe_typing.cmx \
+    proofs/tacinterp.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
+    toplevel/vernac.cmx toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \
     contrib/correctness/psyntax.cmi 
 contrib/correctness/ptactic.cmo: library/declare.cmi tactics/equality.cmi \
     pretyping/evd.cmi library/global.cmi kernel/names.cmi library/nametab.cmi \
@@ -1781,19 +1791,19 @@ contrib/correctness/ptyping.cmx: parsing/ast.cmx parsing/astterm.cmx \
     pretyping/reductionops.cmx kernel/term.cmx pretyping/termops.cmx \
     pretyping/typing.cmx lib/util.cmx contrib/correctness/ptyping.cmi 
 contrib/correctness/putil.cmo: parsing/coqlib.cmi kernel/environ.cmi \
-    library/global.cmi kernel/names.cmi contrib/correctness/past.cmi \
-    pretyping/pattern.cmi contrib/correctness/peffect.cmi \
-    contrib/correctness/penv.cmi contrib/correctness/pmisc.cmi lib/pp.cmi \
-    contrib/correctness/prename.cmi parsing/printer.cmi \
-    contrib/correctness/ptype.cmi kernel/term.cmi pretyping/termops.cmi \
-    lib/util.cmi contrib/correctness/putil.cmi 
+    library/global.cmi library/nameops.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi pretyping/pattern.cmi \
+    contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi lib/pp.cmi contrib/correctness/prename.cmi \
+    parsing/printer.cmi contrib/correctness/ptype.cmi kernel/term.cmi \
+    pretyping/termops.cmi lib/util.cmi contrib/correctness/putil.cmi 
 contrib/correctness/putil.cmx: parsing/coqlib.cmx kernel/environ.cmx \
-    library/global.cmx kernel/names.cmx contrib/correctness/past.cmi \
-    pretyping/pattern.cmx contrib/correctness/peffect.cmx \
-    contrib/correctness/penv.cmx contrib/correctness/pmisc.cmx lib/pp.cmx \
-    contrib/correctness/prename.cmx parsing/printer.cmx \
-    contrib/correctness/ptype.cmi kernel/term.cmx pretyping/termops.cmx \
-    lib/util.cmx contrib/correctness/putil.cmi 
+    library/global.cmx library/nameops.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi pretyping/pattern.cmx \
+    contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx lib/pp.cmx contrib/correctness/prename.cmx \
+    parsing/printer.cmx contrib/correctness/ptype.cmi kernel/term.cmx \
+    pretyping/termops.cmx lib/util.cmx contrib/correctness/putil.cmi 
 contrib/correctness/pwp.cmo: kernel/environ.cmi library/global.cmi \
     kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
     contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -1828,16 +1838,18 @@ contrib/extraction/extract_env.cmo: parsing/astterm.cmi \
     contrib/extraction/common.cmi pretyping/evd.cmi \
     contrib/extraction/extraction.cmi library/global.cmi library/lib.cmi \
     library/libobject.cmi library/library.cmi contrib/extraction/miniml.cmi \
-    contrib/extraction/mlutil.cmi kernel/names.cmi library/nametab.cmi \
-    lib/pp.cmi contrib/extraction/table.cmi kernel/term.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi contrib/extraction/extract_env.cmi 
+    contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi contrib/extraction/table.cmi \
+    kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+    contrib/extraction/extract_env.cmi 
 contrib/extraction/extract_env.cmx: parsing/astterm.cmx \
     contrib/extraction/common.cmx pretyping/evd.cmx \
     contrib/extraction/extraction.cmx library/global.cmx library/lib.cmx \
     library/libobject.cmx library/library.cmx contrib/extraction/miniml.cmi \
-    contrib/extraction/mlutil.cmx kernel/names.cmx library/nametab.cmx \
-    lib/pp.cmx contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx contrib/extraction/extract_env.cmi 
+    contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx contrib/extraction/table.cmx \
+    kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+    contrib/extraction/extract_env.cmi 
 contrib/extraction/extraction.cmo: kernel/closure.cmi kernel/declarations.cmi \
     kernel/environ.cmi pretyping/evd.cmi library/global.cmi lib/gmap.cmi \
     kernel/inductive.cmi pretyping/instantiate.cmi \
@@ -2034,6 +2046,14 @@ contrib/interface/pbp.cmx: parsing/coqlib.cmx contrib/interface/ctast.cmx \
     kernel/reduction.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
     tactics/tacticals.cmx tactics/tactics.cmx kernel/term.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: parsing/ast.cmi parsing/astterm.cmi \
     proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \
     kernel/environ.cmi pretyping/evd.cmi library/global.cmi \
@@ -2054,14 +2074,6 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \
     kernel/term.cmx parsing/termast.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 \
     contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi library/libobject.cmi library/library.cmi \
@@ -2158,8 +2170,6 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
     parsing/printer.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/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/environ.cmi pretyping/evd.cmi library/global.cmi library/lib.cmi \
     library/libobject.cmi library/library.cmi library/nameops.cmi \
@@ -2180,6 +2190,8 @@ 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 
 tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 contrib/correctness/psyntax.cmo: parsing/grammar.cma
 contrib/field/field.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 3672e35d4..6b7d42d89 100644
--- a/doc/kernel.dep.ps
+++ b/doc/kernel.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 577 73
diff --git a/doc/library.dep.ps b/doc/library.dep.ps
index eb358f772..f79236717 100644
--- a/doc/library.dep.ps
+++ b/doc/library.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 543 235
diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps
index 9df862840..9a6de4273 100644
--- a/doc/parsing.dep.ps
+++ b/doc/parsing.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 576 232
diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps
index 8af063428..9246e91a5 100644
--- a/doc/pretyping.dep.ps
+++ b/doc/pretyping.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 577 203
diff --git a/doc/proofs.dep.ps b/doc/proofs.dep.ps
index 28297b5aa..29c50d955 100644
--- a/doc/proofs.dep.ps
+++ b/doc/proofs.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 577 124
+%%BoundingBox: 36 36 577 136
 %%EndComments
 %%BeginProlog
 save
@@ -150,205 +150,225 @@ def
 %%EndResource
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 124
+%%PageBoundingBox: 36 36 577 136
 %%PageOrientation: Portrait
 gsave
-35 35 542 89 boxprim clip newpath
+35 35 542 101 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.6067 set_scale
+0.6905 set_scale
 0 0 translate 0 rotate
-[ /CropBox [36 36 577 124] /PAGES pdfmark
+[ /CropBox [36 36 577 136] /PAGES pdfmark
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Tactic_debug
 gsave 10 dict begin
-167 126 48 18 ellipse_path
+167 18 48 18 ellipse_path
 stroke
 gsave 10 dict begin
-167 127 moveto (Tactic_debug) 76 14.00 -0.50 alignedtext
+167 19 moveto (Tactic_debug) 76 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tacmach
 gsave 10 dict begin
-288 72 36 18 ellipse_path
+298 72 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-288 73 moveto (Tacmach) 51 14.00 -0.50 alignedtext
+298 73 moveto (Tacmach) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tactic_debug -> Tacmach
-newpath 198 112 moveto
-215 104 235 95 252 88 curveto
+newpath 200 31 moveto
+219 39 243 49 262 57 curveto
 stroke
-newpath 251 86 moveto
-261 84 lineto
-253 90 lineto
+newpath 262 54 moveto
+270 60 lineto
+260 59 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Evar_refiner
+%	Refiner
 gsave 10 dict begin
-406 72 45 18 ellipse_path
+411 99 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-406 73 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
+411 100 moveto (Refiner) 41 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Tacmach -> Evar_refiner
-newpath 324 72 moveto
-332 72 341 72 350 72 curveto
+%	Tacmach -> Refiner
+newpath 331 80 moveto
+344 83 360 87 373 90 curveto
 stroke
-newpath 350 70 moveto
-360 72 lineto
-350 75 lineto
+newpath 373 87 moveto
+382 92 lineto
+372 92 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Refiner
+%	Logic
 gsave 10 dict begin
-519 72 31 18 ellipse_path
+505 99 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-519 73 moveto (Refiner) 41 14.00 -0.50 alignedtext
+505 100 moveto (Logic) 32 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Evar_refiner -> Refiner
-newpath 452 72 moveto
-461 72 470 72 478 72 curveto
+%	Refiner -> Logic
+newpath 442 99 moveto
+450 99 459 99 468 99 curveto
 stroke
-newpath 478 70 moveto
-488 72 lineto
-478 75 lineto
+newpath 468 97 moveto
+478 99 lineto
+468 102 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Tacinterp
 gsave 10 dict begin
-45 99 37 18 ellipse_path
+45 72 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-45 100 moveto (Tacinterp) 53 14.00 -0.50 alignedtext
+45 73 moveto (Tacinterp) 53 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tacinterp -> Tactic_debug
-newpath 79 107 moveto
-90 109 103 112 115 115 curveto
+newpath 72 60 moveto
+88 53 109 44 127 36 curveto
 stroke
-newpath 116 113 moveto
-125 117 lineto
-115 117 lineto
+newpath 126 34 moveto
+136 32 lineto
+128 38 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pfedit
 gsave 10 dict begin
-167 72 27 18 ellipse_path
+167 126 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-167 73 moveto (Pfedit) 33 14.00 -0.50 alignedtext
+167 127 moveto (Pfedit) 33 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tacinterp -> Pfedit
-newpath 79 91 moveto
-96 88 116 83 132 80 curveto
+newpath 72 84 moveto
+91 93 117 104 136 112 curveto
 stroke
-newpath 131 78 moveto
-141 78 lineto
-132 83 lineto
+newpath 136 109 moveto
+144 116 lineto
+134 114 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pfedit -> Tacmach
-newpath 194 72 moveto
-208 72 226 72 242 72 curveto
+newpath 190 116 moveto
+210 108 239 96 261 87 curveto
 stroke
-newpath 242 70 moveto
-252 72 lineto
-242 75 lineto
+newpath 260 85 moveto
+270 83 lineto
+262 89 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Logic
+%	Evar_refiner
 gsave 10 dict begin
-613 72 27 18 ellipse_path
+298 126 45 18 ellipse_path
 stroke
 gsave 10 dict begin
-613 73 moveto (Logic) 32 14.00 -0.50 alignedtext
+298 127 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Refiner -> Logic
-newpath 550 72 moveto
-558 72 567 72 576 72 curveto
+%	Pfedit -> Evar_refiner
+newpath 194 126 moveto
+208 126 226 126 242 126 curveto
 stroke
-newpath 576 70 moveto
-586 72 lineto
-576 75 lineto
+newpath 242 124 moveto
+252 126 lineto
+242 129 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Proof_trees
 gsave 10 dict begin
-719 72 42 18 ellipse_path
+611 99 42 18 ellipse_path
 stroke
 gsave 10 dict begin
-719 73 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
+611 100 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Logic -> Proof_trees
-newpath 640 72 moveto
-648 72 657 72 666 72 curveto
+newpath 532 99 moveto
+540 99 549 99 558 99 curveto
 stroke
-newpath 666 70 moveto
-676 72 lineto
-666 75 lineto
+newpath 558 97 moveto
+568 99 lineto
+558 102 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Proof_type
 gsave 10 dict begin
-840 72 41 18 ellipse_path
+732 99 41 18 ellipse_path
 stroke
 gsave 10 dict begin
-840 73 moveto (Proof_type) 62 14.00 -0.50 alignedtext
+732 100 moveto (Proof_type) 62 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Proof_trees -> Proof_type
-newpath 762 72 moveto
-771 72 780 72 788 72 curveto
+newpath 654 99 moveto
+663 99 672 99 680 99 curveto
 stroke
-newpath 788 70 moveto
-798 72 lineto
-788 75 lineto
+newpath 680 97 moveto
+690 99 lineto
+680 102 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Evar_refiner -> Refiner
+newpath 337 117 moveto
+349 114 362 111 373 108 curveto
+stroke
+newpath 372 106 moveto
+382 106 lineto
+373 111 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Clenv
 gsave 10 dict begin
-167 18 27 18 ellipse_path
+167 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-167 19 moveto (Clenv) 33 14.00 -0.50 alignedtext
+167 73 moveto (Clenv) 33 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Clenv -> Tacmach
-newpath 189 28 moveto
-206 36 232 48 252 56 curveto
+newpath 194 72 moveto
+211 72 232 72 252 72 curveto
+stroke
+newpath 252 70 moveto
+262 72 lineto
+252 75 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Clenv -> Evar_refiner
+newpath 190 82 moveto
+208 89 235 100 257 109 curveto
 stroke
-newpath 253 54 moveto
-261 60 lineto
-251 58 lineto
+newpath 258 107 moveto
+266 113 lineto
+256 111 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps
index a628a56d9..0ec3a8272 100644
--- a/doc/tactics.dep.ps
+++ b/doc/tactics.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 577 125
diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps
index 725910c85..44a92446d 100644
--- a/doc/toplevel.dep.ps
+++ b/doc/toplevel.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 576 256
@@ -164,416 +164,404 @@ gsave
 
 %	Vernac
 gsave 10 dict begin
-542 226 30 18 ellipse_path
+542 126 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-542 227 moveto (Vernac) 40 14.00 -0.50 alignedtext
+542 127 moveto (Vernac) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacinterp
 gsave 10 dict begin
-695 234 46 18 ellipse_path
+695 118 46 18 ellipse_path
 stroke
 gsave 10 dict begin
-695 235 moveto (Vernacinterp) 72 14.00 -0.50 alignedtext
+695 119 moveto (Vernacinterp) 72 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernac -> Vernacinterp
-newpath 573 228 moveto
-592 229 619 230 642 231 curveto
+newpath 573 124 moveto
+592 123 619 122 642 121 curveto
 stroke
-newpath 639 228 moveto
-649 232 lineto
-639 233 lineto
+newpath 639 119 moveto
+649 120 lineto
+639 124 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Command
 gsave 10 dict begin
-818 203 39 18 ellipse_path
+818 155 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-818 204 moveto (Command) 58 14.00 -0.50 alignedtext
+818 156 moveto (Command) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacinterp -> Command
-newpath 734 224 moveto
-747 221 761 218 774 214 curveto
+newpath 732 129 moveto
+746 133 761 138 776 142 curveto
 stroke
-newpath 773 212 moveto
-783 212 lineto
-774 217 lineto
+newpath 776 139 moveto
+785 145 lineto
+775 144 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Himsg
 gsave 10 dict begin
-818 257 29 18 ellipse_path
+818 78 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-818 258 moveto (Himsg) 37 14.00 -0.50 alignedtext
+818 79 moveto (Himsg) 37 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacinterp -> Himsg
-newpath 737 242 moveto
-752 244 767 248 781 250 curveto
+newpath 731 106 moveto
+748 101 768 94 784 89 curveto
 stroke
-newpath 781 247 moveto
-790 252 lineto
-780 252 lineto
+newpath 782 87 moveto
+792 86 lineto
+784 92 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Vernacentries
 gsave 10 dict begin
-542 126 49 18 ellipse_path
+542 226 49 18 ellipse_path
 stroke
 gsave 10 dict begin
-542 127 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
+542 227 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Vernacinterp
-newpath 562 143 moveto
-586 162 624 193 648 210 curveto
-651 212 655 215 660 217 curveto
+newpath 562 209 moveto
+586 190 624 159 648 142 curveto
+651 140 655 137 660 135 curveto
 stroke
-newpath 658 213 moveto
-666 220 lineto
-656 218 lineto
+newpath 656 134 moveto
+666 132 lineto
+658 139 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Discharge
 gsave 10 dict begin
-695 126 38 18 ellipse_path
+695 280 38 18 ellipse_path
 stroke
 gsave 10 dict begin
-695 127 moveto (Discharge) 56 14.00 -0.50 alignedtext
+695 281 moveto (Discharge) 56 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Discharge
-newpath 591 126 moveto
-609 126 629 126 647 126 curveto
+newpath 577 239 moveto
+601 247 631 257 656 266 curveto
 stroke
-newpath 646 124 moveto
-656 126 lineto
-646 129 lineto
+newpath 656 263 moveto
+664 269 lineto
+654 268 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Metasyntax
 gsave 10 dict begin
-695 72 43 18 ellipse_path
+695 226 43 18 ellipse_path
 stroke
 gsave 10 dict begin
-695 73 moveto (Metasyntax) 65 14.00 -0.50 alignedtext
+695 227 moveto (Metasyntax) 65 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Metasyntax
-newpath 577 113 moveto
-600 106 630 96 653 87 curveto
+newpath 591 226 moveto
+608 226 626 226 642 226 curveto
 stroke
-newpath 652 85 moveto
-662 84 lineto
-653 90 lineto
+newpath 642 224 moveto
+652 226 lineto
+642 229 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Mltop
 gsave 10 dict begin
-695 18 27 18 ellipse_path
+695 334 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-695 19 moveto (Mltop) 34 14.00 -0.50 alignedtext
+695 335 moveto (Mltop) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Mltop
-newpath 562 109 moveto
-586 90 624 59 648 42 curveto
-653 39 659 35 666 32 curveto
+newpath 562 243 moveto
+586 262 624 293 648 310 curveto
+653 313 659 317 666 320 curveto
 stroke
-newpath 662 31 moveto
-672 29 lineto
-664 36 lineto
+newpath 664 316 moveto
+672 323 lineto
+662 321 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Record
 gsave 10 dict begin
-695 180 30 18 ellipse_path
+695 172 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-695 181 moveto (Record) 40 14.00 -0.50 alignedtext
+695 173 moveto (Record) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Record
-newpath 577 139 moveto
-602 147 636 159 661 168 curveto
+newpath 577 213 moveto
+602 205 636 193 661 184 curveto
 stroke
-newpath 661 165 moveto
-669 171 lineto
-659 170 lineto
+newpath 659 182 moveto
+669 181 lineto
+661 187 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Class
 gsave 10 dict begin
-818 149 27 18 ellipse_path
+818 220 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-818 150 moveto (Class) 30 14.00 -0.50 alignedtext
+818 221 moveto (Class) 30 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Discharge -> Class
-newpath 731 133 moveto
-747 136 766 140 783 142 curveto
+newpath 722 267 moveto
+741 257 768 245 788 235 curveto
 stroke
-newpath 783 139 moveto
-792 144 lineto
-782 144 lineto
+newpath 786 233 moveto
+796 231 lineto
+788 238 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Recordobj
 gsave 10 dict begin
-818 95 39 18 ellipse_path
+818 280 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-818 96 moveto (Recordobj) 58 14.00 -0.50 alignedtext
+818 281 moveto (Recordobj) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Discharge -> Recordobj
-newpath 729 117 moveto
-743 114 759 110 774 106 curveto
+newpath 734 280 moveto
+745 280 757 280 768 280 curveto
 stroke
-newpath 773 104 moveto
-783 104 lineto
-774 109 lineto
+newpath 768 278 moveto
+778 280 lineto
+768 283 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Record -> Command
-newpath 724 185 moveto
-738 187 756 191 771 194 curveto
+newpath 725 168 moveto
+738 166 755 164 770 162 curveto
 stroke
-newpath 772 192 moveto
-781 196 lineto
-771 196 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Record -> Himsg
-newpath 718 192 moveto
-730 198 742 204 742 204 curveto
-755 212 766 224 778 233 curveto
-781 235 786 238 791 240 curveto
-stroke
-newpath 790 236 moveto
-797 244 lineto
-787 241 lineto
+newpath 770 160 moveto
+780 160 lineto
+771 164 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Record -> Class
-newpath 723 173 moveto
-741 169 764 163 784 158 curveto
+newpath 720 182 moveto
+739 189 765 199 786 207 curveto
 stroke
-newpath 783 156 moveto
-793 156 lineto
-784 161 lineto
+newpath 786 204 moveto
+794 211 lineto
+784 209 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Toplevel
 gsave 10 dict begin
-247 122 35 18 ellipse_path
+247 199 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-247 123 moveto (Toplevel) 49 14.00 -0.50 alignedtext
+247 200 moveto (Toplevel) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Toplevel -> Mltop
-newpath 279 115 moveto
-361 96 578 45 662 26 curveto
+newpath 277 208 moveto
+359 233 579 299 663 324 curveto
 stroke
-newpath 659 24 moveto
-669 24 lineto
-660 29 lineto
+newpath 661 321 moveto
+670 326 lineto
+660 326 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Protectedtoplevel
 gsave 10 dict begin
-377 253 59 18 ellipse_path
+377 99 59 18 ellipse_path
 stroke
 gsave 10 dict begin
-377 254 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
+377 100 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Toplevel -> Protectedtoplevel
-newpath 263 138 moveto
-286 161 328 204 355 231 curveto
+newpath 266 184 moveto
+288 168 322 141 347 122 curveto
 stroke
-newpath 355 227 moveto
-360 236 lineto
-351 231 lineto
+newpath 346 120 moveto
+355 116 lineto
+349 124 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Protectedtoplevel -> Vernac
-newpath 429 244 moveto
-454 240 481 236 503 232 curveto
+newpath 429 108 moveto
+454 112 481 116 503 120 curveto
 stroke
-newpath 502 230 moveto
-512 231 lineto
-502 235 lineto
+newpath 502 117 moveto
+512 121 lineto
+502 122 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Errors
 gsave 10 dict begin
-542 280 27 18 ellipse_path
+542 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-542 281 moveto (Errors) 34 14.00 -0.50 alignedtext
+542 73 moveto (Errors) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Protectedtoplevel -> Errors
-newpath 429 262 moveto
-455 266 484 271 507 274 curveto
+newpath 429 90 moveto
+455 86 484 81 507 78 curveto
 stroke
-newpath 505 271 moveto
-515 275 lineto
-505 276 lineto
+newpath 505 76 moveto
+515 77 lineto
+505 81 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Line_oriented_parser
 gsave 10 dict begin
-542 334 70 18 ellipse_path
+542 18 70 18 ellipse_path
 stroke
 gsave 10 dict begin
-542 335 moveto (Line_oriented_parser) 119 14.00 -0.50 alignedtext
+542 19 moveto (Line_oriented_parser) 119 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Protectedtoplevel -> Line_oriented_parser
-newpath 403 269 moveto
-424 282 453 300 472 310 curveto
-477 312 484 315 491 318 curveto
+newpath 403 83 moveto
+424 70 453 52 472 42 curveto
+477 40 484 37 491 34 curveto
 stroke
-newpath 489 315 moveto
-498 320 lineto
-488 320 lineto
+newpath 488 32 moveto
+498 32 lineto
+489 37 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Errors -> Himsg
-newpath 569 278 moveto
-619 274 725 265 781 260 curveto
+newpath 570 73 moveto
+620 74 725 76 781 77 curveto
 stroke
-newpath 779 258 moveto
-789 259 lineto
-779 263 lineto
+newpath 779 75 moveto
+789 77 lineto
+779 80 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Minicoq
 gsave 10 dict begin
-42 230 34 18 ellipse_path
+42 253 34 18 ellipse_path
 stroke
 gsave 10 dict begin
-42 231 moveto (Minicoq) 47 14.00 -0.50 alignedtext
+42 254 moveto (Minicoq) 47 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Fhimsg
 gsave 10 dict begin
-144 230 31 18 ellipse_path
+144 253 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-144 231 moveto (Fhimsg) 42 14.00 -0.50 alignedtext
+144 254 moveto (Fhimsg) 42 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Minicoq -> Fhimsg
-newpath 76 230 moveto
-85 230 94 230 102 230 curveto
+newpath 76 253 moveto
+85 253 94 253 102 253 curveto
 stroke
-newpath 102 228 moveto
-112 230 lineto
-102 233 lineto
+newpath 102 251 moveto
+112 253 lineto
+102 256 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coqtop
 gsave 10 dict begin
-42 149 31 18 ellipse_path
+42 172 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-42 150 moveto (Coqtop) 41 14.00 -0.50 alignedtext
+42 173 moveto (Coqtop) 41 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqinit
 gsave 10 dict begin
-144 122 31 18 ellipse_path
+144 199 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-144 123 moveto (Coqinit) 42 14.00 -0.50 alignedtext
+144 200 moveto (Coqinit) 42 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqtop -> Coqinit
-newpath 70 141 moveto
-81 138 94 135 106 132 curveto
+newpath 70 180 moveto
+81 183 94 186 106 189 curveto
 stroke
-newpath 105 130 moveto
-115 129 lineto
-106 135 lineto
+newpath 106 186 moveto
+115 192 lineto
+105 191 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Usage
 gsave 10 dict begin
-144 176 27 18 ellipse_path
+144 145 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-144 177 moveto (Usage) 34 14.00 -0.50 alignedtext
+144 146 moveto (Usage) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqtop -> Usage
-newpath 70 157 moveto
-82 160 96 164 109 167 curveto
+newpath 70 164 moveto
+82 161 96 157 109 154 curveto
 stroke
-newpath 109 164 moveto
-118 169 lineto
-108 169 lineto
+newpath 108 152 moveto
+118 152 lineto
+109 157 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coqinit -> Toplevel
-newpath 176 122 moveto
-184 122 193 122 202 122 curveto
+newpath 176 199 moveto
+184 199 193 199 202 199 curveto
 stroke
-newpath 202 120 moveto
-212 122 lineto
-202 125 lineto
+newpath 202 197 moveto
+212 199 lineto
+202 202 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
author	clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7>	2001-11-29 13:38:18 +0000
committer	clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7>	2001-11-29 13:38:18 +0000
commit	28d905bd62786e0938cd333ddcdc2f7754dd0165 (patch)
tree	3ec3990196d8e80c59d0b595dbac61c3adf63100
parent	476d1f90525a97f18fa1c2adbde453f5e1e9213c (diff)