New version of functional induction / inversion. By Julien Forest,

Benjamin Gregoire, Gilles Barthe.

For the moment, it is as followed:

If one uses GenFixpoint instead of Fixpoint, then induction principles
are generated on the fly (respecting the match structure written by
the user, with wildcards etc). These principles can be used directly
or by tactics "new functional induction" and "functional inversion".

We will soon make "new functional induction" become "functional
induction", before release of V8.1.


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

1 files changed, 251 insertions, 171 deletions

diff --git a/.depend b/.depend
index 6323a4810..69b828ae6 100644
--- a/.depend
+++ b/.depend
@@ -54,12 +54,12 @@ kernel/indtypes.cmi: kernel/univ.cmi kernel/typeops.cmi kernel/term.cmi \
     kernel/declarations.cmi 
 kernel/inductive.cmi: kernel/univ.cmi kernel/term.cmi kernel/names.cmi \
     kernel/environ.cmi kernel/declarations.cmi 
-kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi 
-kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \
-    kernel/declarations.cmi 
 kernel/modops.cmi: lib/util.cmi kernel/univ.cmi kernel/names.cmi \
     kernel/mod_subst.cmi kernel/environ.cmi kernel/entries.cmi \
     kernel/declarations.cmi 
+kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi 
+kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \
+    kernel/declarations.cmi 
 kernel/names.cmi: lib/predicate.cmi lib/pp.cmi 
 kernel/pre_env.cmi: lib/util.cmi kernel/univ.cmi kernel/term.cmi \
     kernel/sign.cmi kernel/names.cmi kernel/declarations.cmi 
@@ -85,9 +85,6 @@ kernel/vm.cmi: kernel/term.cmi kernel/names.cmi kernel/cemitcodes.cmi \
     kernel/cbytecodes.cmi 
 lib/bigint.cmi: lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
-lib/rtree.cmi: lib/pp.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi lib/compat.cmo 
 library/declare.cmi: kernel/term.cmi kernel/sign.cmi kernel/safe_typing.cmi \
     library/nametab.cmi kernel/names.cmi library/libnames.cmi \
     kernel/indtypes.cmi kernel/environ.cmi kernel/entries.cmi \
@@ -118,6 +115,9 @@ library/library.cmi: lib/util.cmi lib/system.cmi lib/pp.cmi kernel/names.cmi \
 library/nameops.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi 
 library/nametab.cmi: lib/util.cmi lib/pp.cmi kernel/names.cmi \
     library/libnames.cmi 
+lib/rtree.cmi: lib/pp.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi lib/compat.cmo 
 parsing/egrammar.cmi: toplevel/vernacexpr.cmo lib/util.cmi \
     interp/topconstr.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \
     interp/ppextend.cmi parsing/pcoq.cmi kernel/names.cmi \
@@ -345,11 +345,11 @@ toplevel/record.cmi: toplevel/vernacexpr.cmo interp/topconstr.cmi \
 toplevel/searchisos.cmi: kernel/term.cmi kernel/names.cmi \
     library/libobject.cmi 
 toplevel/toplevel.cmi: lib/pp.cmi parsing/pcoq.cmi 
-toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi 
 toplevel/vernacentries.cmi: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
     interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \
     library/libnames.cmi pretyping/evd.cmi kernel/environ.cmi 
 toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
+toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi 
 toplevel/whelp.cmi: interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \
     kernel/environ.cmi 
 contrib/cc/ccalgo.cmi: lib/util.cmi kernel/term.cmi lib/pp.cmi \
@@ -358,9 +358,9 @@ contrib/cc/ccproof.cmi: kernel/names.cmi contrib/cc/ccalgo.cmi
 contrib/cc/cctac.cmi: kernel/term.cmi proofs/proof_type.cmi 
 contrib/correctness/past.cmi: lib/util.cmi interp/topconstr.cmi \
     kernel/term.cmi kernel/names.cmi 
-contrib/correctness/pcic.cmi: pretyping/rawterm.cmi 
 contrib/correctness/pcicenv.cmi: kernel/term.cmi kernel/sign.cmi \
     kernel/names.cmi 
+contrib/correctness/pcic.cmi: pretyping/rawterm.cmi 
 contrib/correctness/pdb.cmi: kernel/names.cmi 
 contrib/correctness/peffect.cmi: lib/pp.cmi kernel/names.cmi 
 contrib/correctness/penv.cmi: kernel/term.cmi kernel/names.cmi \
@@ -380,8 +380,8 @@ contrib/correctness/ptyping.cmi: interp/topconstr.cmi kernel/term.cmi \
     kernel/names.cmi 
 contrib/correctness/putil.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi 
 contrib/correctness/pwp.cmi: kernel/term.cmi 
-contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi 
 contrib/dp/dp_cvcl.cmi: contrib/dp/fol.cmi 
+contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi 
 contrib/dp/dp_simplify.cmi: contrib/dp/fol.cmi 
 contrib/dp/dp_sorts.cmi: contrib/dp/fol.cmi 
 contrib/dp/dp_zenon.cmi: contrib/dp/fol.cmi 
@@ -507,6 +507,14 @@ ide/config_lexer.cmo: lib/util.cmi ide/config_parser.cmi
 ide/config_lexer.cmx: lib/util.cmx ide/config_parser.cmx 
 ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi 
 ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi 
+ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \
+    lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \
+    ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \
+    ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi 
+ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \
+    lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \
+    ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \
+    ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi 
 ide/coq.cmo: toplevel/vernacexpr.cmo toplevel/vernacentries.cmi \
     toplevel/vernac.cmi lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
     proofs/tacmach.cmi tactics/tacinterp.cmi library/states.cmi \
@@ -531,14 +539,6 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \
     ide/coq.cmi 
 ide/coq_tactics.cmo: ide/coq_tactics.cmi 
 ide/coq_tactics.cmx: ide/coq_tactics.cmi 
-ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \
-    lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \
-    ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \
-    ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi 
-ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \
-    lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \
-    ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \
-    ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi 
 ide/find_phrase.cmo: ide/ideutils.cmi 
 ide/find_phrase.cmx: ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmi 
@@ -717,6 +717,14 @@ kernel/inductive.cmo: lib/util.cmi kernel/univ.cmi kernel/type_errors.cmi \
 kernel/inductive.cmx: lib/util.cmx kernel/univ.cmx kernel/type_errors.cmx \
     kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx kernel/names.cmx \
     kernel/environ.cmx kernel/declarations.cmx kernel/inductive.cmi 
+kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \
+    kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \
+    kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \
+    kernel/modops.cmi 
+kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \
+    kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \
+    kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \
+    kernel/modops.cmi 
 kernel/mod_subst.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi \
     kernel/names.cmi kernel/mod_subst.cmi 
 kernel/mod_subst.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx \
@@ -731,14 +739,6 @@ kernel/mod_typing.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \
     kernel/names.cmx kernel/modops.cmx kernel/mod_subst.cmx \
     kernel/environ.cmx kernel/entries.cmx kernel/declarations.cmx \
     kernel/cemitcodes.cmx kernel/mod_typing.cmi 
-kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \
-    kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \
-    kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \
-    kernel/modops.cmi 
-kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \
-    kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \
-    kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \
-    kernel/modops.cmi 
 kernel/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/hashcons.cmi \
     kernel/names.cmi 
 kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/hashcons.cmx \
@@ -837,10 +837,10 @@ lib/edit.cmo: lib/util.cmi lib/pp.cmi lib/bstack.cmi lib/edit.cmi
 lib/edit.cmx: lib/util.cmx lib/pp.cmx lib/bstack.cmx lib/edit.cmi 
 lib/explore.cmo: lib/explore.cmi 
 lib/explore.cmx: lib/explore.cmi 
-lib/gmap.cmo: lib/gmap.cmi 
-lib/gmap.cmx: lib/gmap.cmi 
 lib/gmapl.cmo: lib/util.cmi lib/gmap.cmi lib/gmapl.cmi 
 lib/gmapl.cmx: lib/util.cmx lib/gmap.cmx lib/gmapl.cmi 
+lib/gmap.cmo: lib/gmap.cmi 
+lib/gmap.cmx: lib/gmap.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
@@ -849,26 +849,14 @@ lib/heap.cmo: lib/heap.cmi
 lib/heap.cmx: lib/heap.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/pp_control.cmo: lib/pp_control.cmi 
 lib/pp_control.cmx: lib/pp_control.cmi 
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/predicate.cmo: lib/predicate.cmi 
 lib/predicate.cmx: lib/predicate.cmi 
 lib/profile.cmo: lib/profile.cmi 
 lib/profile.cmx: lib/profile.cmi 
-lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi 
-lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi 
-lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi 
-library/decl_kinds.cmo: lib/util.cmi 
-library/decl_kinds.cmx: lib/util.cmx 
 library/declare.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \
     kernel/type_errors.cmi kernel/term.cmi library/summary.cmi \
     kernel/sign.cmi kernel/safe_typing.cmi kernel/reduction.cmi lib/pp.cmi \
@@ -901,6 +889,8 @@ library/declaremods.cmx: lib/util.cmx library/summary.cmx \
     library/libobject.cmx library/libnames.cmx library/lib.cmx \
     library/global.cmx kernel/environ.cmx kernel/entries.cmx \
     kernel/declarations.cmx library/declaremods.cmi 
+library/decl_kinds.cmo: lib/util.cmi 
+library/decl_kinds.cmx: lib/util.cmx 
 library/dischargedhypsmap.cmo: lib/util.cmi kernel/term.cmi \
     library/summary.cmi kernel/reduction.cmi library/nametab.cmi \
     kernel/names.cmi library/libobject.cmi library/libnames.cmi \
@@ -983,6 +973,16 @@ library/states.cmx: lib/system.cmx library/summary.cmx library/library.cmx \
     library/lib.cmx library/states.cmi 
 library/summary.cmo: lib/util.cmi lib/pp.cmi lib/dyn.cmi library/summary.cmi 
 library/summary.cmx: lib/util.cmx lib/pp.cmx lib/dyn.cmx library/summary.cmi 
+lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi 
+lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi 
+lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi 
 parsing/argextend.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     parsing/q_util.cmi parsing/q_coqast.cmo parsing/pcoq.cmi \
     interp/genarg.cmi 
@@ -2051,8 +2051,6 @@ tactics/termdn.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \
     pretyping/pattern.cmx library/nametab.cmx kernel/names.cmx \
     library/nameops.cmx library/libnames.cmx tactics/dn.cmx \
     tactics/termdn.cmi 
-test-suite/zarith.cmo: test-suite/zarith.cmi 
-test-suite/zarith.cmx: test-suite/zarith.cmi 
 tools/coqdep.cmo: tools/coqdep_lexer.cmo config/coq_config.cmi 
 tools/coqdep.cmx: tools/coqdep_lexer.cmx config/coq_config.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
@@ -2239,16 +2237,6 @@ toplevel/toplevel.cmx: toplevel/vernacexpr.cmx toplevel/vernac.cmx \
     toplevel/toplevel.cmi 
 toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi 
 toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi 
-toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
-    toplevel/vernacentries.cmi lib/util.cmi lib/system.cmi library/states.cmi \
-    parsing/ppvernac.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \
-    lib/options.cmi kernel/names.cmi library/library.cmi library/lib.cmi \
-    parsing/lexer.cmi interp/constrintern.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
-    toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \
-    parsing/ppvernac.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \
-    lib/options.cmx kernel/names.cmx library/library.cmx library/lib.cmx \
-    parsing/lexer.cmx interp/constrintern.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: kernel/vm.cmi toplevel/vernacinterp.cmi \
     toplevel/vernacexpr.cmo kernel/vconv.cmi lib/util.cmi kernel/univ.cmi \
     kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
@@ -2309,6 +2297,16 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/proof_type.cmx lib/pp.cmx \
     lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \
     toplevel/vernacinterp.cmi 
+toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacentries.cmi lib/util.cmi lib/system.cmi library/states.cmi \
+    parsing/ppvernac.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \
+    lib/options.cmi kernel/names.cmi library/library.cmi library/lib.cmi \
+    parsing/lexer.cmi interp/constrintern.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \
+    parsing/ppvernac.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \
+    lib/options.cmx kernel/names.cmx library/library.cmx library/lib.cmx \
+    parsing/lexer.cmx interp/constrintern.cmx toplevel/vernac.cmi 
 toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi lib/system.cmi \
     interp/syntax_def.cmi proofs/refiner.cmi pretyping/rawterm.cmi lib/pp.cmi \
@@ -2359,6 +2357,12 @@ contrib/cc/g_congruence.cmx: lib/util.cmx tactics/tactics.cmx \
     proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \
     interp/genarg.cmx parsing/egrammar.cmx toplevel/cerrors.cmx \
     contrib/cc/cctac.cmx 
+contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \
+    kernel/sign.cmi kernel/names.cmi library/global.cmi \
+    contrib/correctness/pcicenv.cmi 
+contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \
+    kernel/sign.cmx kernel/names.cmx library/global.cmx \
+    contrib/correctness/pcicenv.cmi 
 contrib/correctness/pcic.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
     kernel/term.cmi kernel/sign.cmi toplevel/record.cmi pretyping/rawterm.cmi \
@@ -2373,12 +2377,6 @@ contrib/correctness/pcic.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     library/libnames.cmx kernel/indtypes.cmx library/global.cmx \
     kernel/entries.cmx pretyping/detyping.cmx library/declare.cmx \
     kernel/declarations.cmx contrib/correctness/pcic.cmi 
-contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \
-    kernel/sign.cmi kernel/names.cmi library/global.cmi \
-    contrib/correctness/pcicenv.cmi 
-contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \
-    kernel/sign.cmx kernel/names.cmx library/global.cmx \
-    contrib/correctness/pcicenv.cmi 
 contrib/correctness/pdb.cmo: pretyping/termops.cmi kernel/term.cmi \
     library/nametab.cmi kernel/names.cmi library/global.cmi \
     interp/constrintern.cmi contrib/correctness/pdb.cmi 
@@ -2499,6 +2497,8 @@ contrib/correctness/pwp.cmx: lib/util.cmx pretyping/termops.cmx \
     library/nametab.cmx kernel/names.cmx library/libnames.cmx \
     tactics/hipattern.cmx library/global.cmx kernel/environ.cmx \
     contrib/correctness/pwp.cmi 
+contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi 
+contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi 
 contrib/dp/dp.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \
     kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
     proofs/tacmach.cmi library/summary.cmi parsing/printer.cmi lib/pp.cmi \
@@ -2517,8 +2517,6 @@ contrib/dp/dp.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \
     contrib/dp/dp_zenon.cmx contrib/dp/dp_sorts.cmx \
     contrib/dp/dp_simplify.cmx contrib/dp/dp_cvcl.cmx kernel/declarations.cmx \
     interp/coqlib.cmx contrib/dp/dp.cmi 
-contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi 
-contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi 
 contrib/dp/dp_simplify.cmo: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi 
 contrib/dp/dp_simplify.cmx: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi 
 contrib/dp/dp_sorts.cmo: contrib/dp/fol.cmi contrib/dp/dp_sorts.cmi 
@@ -2793,6 +2791,114 @@ contrib/fourier/g_fourier.cmx: lib/util.cmx tactics/tacinterp.cmx \
     proofs/tacexpr.cmx proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx \
     parsing/pcoq.cmx contrib/fourier/fourierR.cmx parsing/egrammar.cmx \
     toplevel/cerrors.cmx 
+contrib/funind/indfun_common.cmo: lib/util.cmi kernel/term.cmi \
+    pretyping/rawterm.cmi lib/pp.cmi library/nametab.cmi kernel/names.cmi \
+    library/nameops.cmi library/libnames.cmi library/global.cmi \
+    kernel/declarations.cmi interp/coqlib.cmi 
+contrib/funind/indfun_common.cmx: lib/util.cmx kernel/term.cmx \
+    pretyping/rawterm.cmx lib/pp.cmx library/nametab.cmx kernel/names.cmx \
+    library/nameops.cmx library/libnames.cmx library/global.cmx \
+    kernel/declarations.cmx interp/coqlib.cmx 
+contrib/funind/indfun_main.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
+    interp/topconstr.cmi kernel/term.cmi tactics/tacticals.cmi \
+    tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/refiner.cmi \
+    pretyping/rawterm.cmi parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi \
+    library/nametab.cmi kernel/names.cmi library/nameops.cmi \
+    library/libnames.cmi parsing/lexer.cmi contrib/funind/invfun.cmo \
+    pretyping/indrec.cmi contrib/funind/indfun_common.cmo \
+    contrib/funind/indfun.cmo tactics/hiddentac.cmi interp/genarg.cmi \
+    parsing/g_vernac.cmo parsing/g_constr.cmo parsing/egrammar.cmi \
+    toplevel/cerrors.cmi 
+contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
+    interp/topconstr.cmx kernel/term.cmx tactics/tacticals.cmx \
+    tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/refiner.cmx \
+    pretyping/rawterm.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \
+    library/nametab.cmx kernel/names.cmx library/nameops.cmx \
+    library/libnames.cmx parsing/lexer.cmx contrib/funind/invfun.cmx \
+    pretyping/indrec.cmx contrib/funind/indfun_common.cmx \
+    contrib/funind/indfun.cmx tactics/hiddentac.cmx interp/genarg.cmx \
+    parsing/g_vernac.cmx parsing/g_constr.cmx parsing/egrammar.cmx \
+    toplevel/cerrors.cmx 
+contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
+    interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \
+    library/states.cmi contrib/funind/rawterm_to_relation.cmo \
+    pretyping/rawterm.cmi lib/pp.cmi lib/options.cmi interp/notation.cmi \
+    contrib/funind/new_arg_principle.cmo kernel/names.cmi \
+    library/libnames.cmi pretyping/indrec.cmi \
+    contrib/funind/indfun_common.cmo library/impargs.cmi library/global.cmi \
+    pretyping/evd.cmi kernel/environ.cmi library/decl_kinds.cmo \
+    interp/constrintern.cmi toplevel/command.cmi 
+contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
+    interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \
+    library/states.cmx contrib/funind/rawterm_to_relation.cmx \
+    pretyping/rawterm.cmx lib/pp.cmx lib/options.cmx interp/notation.cmx \
+    contrib/funind/new_arg_principle.cmx kernel/names.cmx \
+    library/libnames.cmx pretyping/indrec.cmx \
+    contrib/funind/indfun_common.cmx library/impargs.cmx library/global.cmx \
+    pretyping/evd.cmx kernel/environ.cmx library/decl_kinds.cmx \
+    interp/constrintern.cmx toplevel/command.cmx 
+contrib/funind/invfun.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \
+    tactics/tacticals.cmi proofs/tacmach.cmi pretyping/rawterm.cmi lib/pp.cmi \
+    kernel/names.cmi library/libnames.cmi pretyping/indrec.cmi \
+    contrib/funind/indfun_common.cmo tactics/hiddentac.cmi \
+    tactics/extratactics.cmi tactics/equality.cmi 
+contrib/funind/invfun.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \
+    tactics/tacticals.cmx proofs/tacmach.cmx pretyping/rawterm.cmx lib/pp.cmx \
+    kernel/names.cmx library/libnames.cmx pretyping/indrec.cmx \
+    contrib/funind/indfun_common.cmx tactics/hiddentac.cmx \
+    tactics/extratactics.cmx tactics/equality.cmx 
+contrib/funind/new_arg_principle.cmo: toplevel/vernacexpr.cmo \
+    toplevel/vernacentries.cmi lib/util.cmi pretyping/unification.cmi \
+    pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \
+    tactics/tacticals.cmi proofs/tactic_debug.cmi pretyping/tacred.cmi \
+    proofs/tacmach.cmi tactics/tacinterp.cmi pretyping/rawterm.cmi \
+    proofs/proof_type.cmi parsing/printer.cmi parsing/ppconstr.cmi lib/pp.cmi \
+    proofs/pfedit.cmi lib/options.cmi library/nametab.cmi kernel/names.cmi \
+    library/libnames.cmi pretyping/indrec.cmi \
+    contrib/funind/indfun_common.cmo tactics/hiddentac.cmi library/global.cmi \
+    interp/genarg.cmi pretyping/evd.cmi tactics/equality.cmi \
+    kernel/environ.cmi kernel/entries.cmi tactics/eauto.cmi \
+    library/declare.cmi kernel/declarations.cmi library/decl_kinds.cmo \
+    interp/coqlib.cmi toplevel/command.cmi kernel/closure.cmi \
+    pretyping/clenv.cmi toplevel/cerrors.cmi contrib/cc/cctac.cmi 
+contrib/funind/new_arg_principle.cmx: toplevel/vernacexpr.cmx \
+    toplevel/vernacentries.cmx lib/util.cmx pretyping/unification.cmx \
+    pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \
+    tactics/tacticals.cmx proofs/tactic_debug.cmx pretyping/tacred.cmx \
+    proofs/tacmach.cmx tactics/tacinterp.cmx pretyping/rawterm.cmx \
+    proofs/proof_type.cmx parsing/printer.cmx parsing/ppconstr.cmx lib/pp.cmx \
+    proofs/pfedit.cmx lib/options.cmx library/nametab.cmx kernel/names.cmx \
+    library/libnames.cmx pretyping/indrec.cmx \
+    contrib/funind/indfun_common.cmx tactics/hiddentac.cmx library/global.cmx \
+    interp/genarg.cmx pretyping/evd.cmx tactics/equality.cmx \
+    kernel/environ.cmx kernel/entries.cmx tactics/eauto.cmx \
+    library/declare.cmx kernel/declarations.cmx library/decl_kinds.cmx \
+    interp/coqlib.cmx toplevel/command.cmx kernel/closure.cmx \
+    pretyping/clenv.cmx toplevel/cerrors.cmx contrib/cc/cctac.cmx 
+contrib/funind/rawtermops.cmo: lib/util.cmi proofs/tactic_debug.cmi \
+    tactics/tacinterp.cmi pretyping/rawterm.cmi parsing/printer.cmi \
+    parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \
+    library/libnames.cmi pretyping/inductiveops.cmi \
+    contrib/funind/indfun_common.cmo library/global.cmi pretyping/evd.cmi \
+    interp/coqlib.cmi 
+contrib/funind/rawtermops.cmx: lib/util.cmx proofs/tactic_debug.cmx \
+    tactics/tacinterp.cmx pretyping/rawterm.cmx parsing/printer.cmx \
+    parsing/ppconstr.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \
+    library/libnames.cmx pretyping/inductiveops.cmx \
+    contrib/funind/indfun_common.cmx library/global.cmx pretyping/evd.cmx \
+    interp/coqlib.cmx 
+contrib/funind/rawterm_to_relation.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
+    interp/topconstr.cmi kernel/term.cmi contrib/funind/rawtermops.cmo \
+    pretyping/rawterm.cmi parsing/printer.cmi parsing/ppvernac.cmi lib/pp.cmi \
+    lib/options.cmi kernel/names.cmi library/nameops.cmi library/libnames.cmi \
+    contrib/funind/indfun_common.cmo library/impargs.cmi interp/coqlib.cmi \
+    interp/constrextern.cmi toplevel/command.cmi toplevel/cerrors.cmi 
+contrib/funind/rawterm_to_relation.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
+    interp/topconstr.cmx kernel/term.cmx contrib/funind/rawtermops.cmx \
+    pretyping/rawterm.cmx parsing/printer.cmx parsing/ppvernac.cmx lib/pp.cmx \
+    lib/options.cmx kernel/names.cmx library/nameops.cmx library/libnames.cmx \
+    contrib/funind/indfun_common.cmx library/impargs.cmx interp/coqlib.cmx \
+    interp/constrextern.cmx toplevel/command.cmx toplevel/cerrors.cmx 
 contrib/funind/tacinv.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \
     tactics/tactics.cmi tactics/tacticals.cmi pretyping/tacred.cmi \
@@ -2989,6 +3095,14 @@ contrib/interface/pbp.cmx: lib/util.cmx pretyping/typing.cmx \
     proofs/logic.cmx library/libnames.cmx tactics/hipattern.cmx \
     library/global.cmx interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
     interp/coqlib.cmx contrib/interface/pbp.cmi 
+contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \
+    contrib/interface/vtp.cmi contrib/interface/translate.cmi \
+    parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \
+    contrib/interface/ascent.cmi 
+contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \
+    contrib/interface/vtp.cmx contrib/interface/translate.cmx \
+    parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \
+    contrib/interface/ascent.cmi 
 contrib/interface/showproof.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/typing.cmi contrib/interface/translate.cmi \
     pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi \
@@ -3011,14 +3125,6 @@ contrib/interface/showproof.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
     kernel/declarations.cmx interp/constrintern.cmx pretyping/clenv.cmx \
     contrib/interface/showproof.cmi 
-contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \
-    contrib/interface/vtp.cmi contrib/interface/translate.cmi \
-    parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \
-    contrib/interface/ascent.cmi 
-contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \
-    contrib/interface/vtp.cmx contrib/interface/translate.cmx \
-    parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \
-    contrib/interface/ascent.cmi 
 contrib/interface/translate.cmo: contrib/interface/xlate.cmi \
     contrib/interface/vtp.cmi toplevel/vernacinterp.cmi lib/util.cmi \
     kernel/term.cmi proofs/tacmach.cmi kernel/sign.cmi proofs/proof_type.cmi \
@@ -3349,18 +3455,12 @@ contrib/subtac/sparser.cmx: toplevel/vernacinterp.cmx \
     parsing/egrammar.cmx toplevel/cerrors.cmx 
 contrib/subtac/sutils.cmo: contrib/subtac/sutils.cmi 
 contrib/subtac/sutils.cmx: contrib/subtac/sutils.cmi 
-contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi 
-contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx 
 contrib/xml/acic2Xml.cmo: contrib/xml/xml.cmi lib/util.cmi kernel/term.cmi \
     kernel/names.cmi contrib/xml/cic2acic.cmo contrib/xml/acic.cmo 
 contrib/xml/acic2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx kernel/term.cmx \
     kernel/names.cmx contrib/xml/cic2acic.cmx contrib/xml/acic.cmx 
-contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \
-    tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \
-    contrib/xml/acic.cmo 
-contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \
-    tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \
-    contrib/xml/acic.cmx 
+contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi 
+contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx 
 contrib/xml/cic2acic.cmo: lib/util.cmi contrib/xml/unshare.cmi \
     kernel/univ.cmi pretyping/termops.cmi kernel/term.cmi \
     pretyping/reductionops.cmi parsing/printer.cmi lib/pp.cmi \
@@ -3379,6 +3479,12 @@ contrib/xml/cic2acic.cmx: lib/util.cmx contrib/xml/unshare.cmx \
     kernel/environ.cmx contrib/xml/doubleTypeInference.cmx \
     library/dischargedhypsmap.cmx library/declare.cmx kernel/declarations.cmx \
     contrib/xml/acic.cmx 
+contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \
+    tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \
+    contrib/xml/acic.cmo 
+contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \
+    tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \
+    contrib/xml/acic.cmx 
 contrib/xml/doubleTypeInference.cmo: lib/util.cmi contrib/xml/unshare.cmi \
     kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \
     pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
@@ -3419,8 +3525,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx \
     contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx contrib/xml/acic.cmx 
 contrib/xml/unshare.cmo: contrib/xml/unshare.cmi 
 contrib/xml/unshare.cmx: contrib/xml/unshare.cmi 
-contrib/xml/xml.cmo: contrib/xml/xml.cmi 
-contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: contrib/xml/xml.cmi toplevel/vernac.cmi \
     lib/util.cmi contrib/xml/unshare.cmi kernel/term.cmi proofs/tacmach.cmi \
     pretyping/recordops.cmi proofs/proof_trees.cmi \
@@ -3451,10 +3555,8 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \
     toplevel/vernacinterp.cmx lib/util.cmx lib/pp.cmx parsing/pcoq.cmx \
     parsing/lexer.cmx interp/genarg.cmx parsing/extend.cmx \
     parsing/egrammar.cmx toplevel/cerrors.cmx 
-ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \
-    ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi 
-ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \
-    ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi 
+contrib/xml/xml.cmo: contrib/xml/xml.cmi 
+contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 ide/utils/configwin_html_config.cmo: ide/utils/uoptions.cmi \
     ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo \
     ide/utils/configwin_ihm.cmo 
@@ -3465,6 +3567,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/uoptions.cmi ide/utils/okey.cmi \
     ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo 
 ide/utils/configwin_ihm.cmx: ide/utils/uoptions.cmx ide/utils/okey.cmx \
     ide/utils/configwin_types.cmx ide/utils/configwin_messages.cmx 
+ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \
+    ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi 
+ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \
+    ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi 
 ide/utils/configwin_types.cmo: ide/utils/uoptions.cmi \
     ide/utils/configwin_keys.cmo 
 ide/utils/configwin_types.cmx: ide/utils/uoptions.cmx \
@@ -3527,6 +3633,8 @@ contrib/funind/tacinv.cmo: parsing/grammar.cma
 contrib/funind/tacinv.cmx: parsing/grammar.cma
 contrib/first-order/g_ground.cmo: parsing/grammar.cma
 contrib/first-order/g_ground.cmx: parsing/grammar.cma
+contrib/funind/indfun_main.cmo: parsing/grammar.cma
+contrib/funind/indfun_main.cmx: parsing/grammar.cma
 contrib/subtac/sparser.cmo: parsing/grammar.cma
 contrib/subtac/sparser.cmx: parsing/grammar.cma
 contrib/subtac/g_eterm.cmo: parsing/grammar.cma
@@ -3588,102 +3696,74 @@ tools/coq_makefile.cmx:
 tools/coq-tex.cmo: 
 tools/coq-tex.cmx: 
 coq_fix_code.o: kernel/byterun/coq_fix_code.c \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
+  /usr/lib/ocaml/3.09.1/caml/config.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/config.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h
 coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/alloc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h \
   kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/alloc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h
 coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
-  kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_values.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h
 coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
+  /usr/lib/ocaml/3.09.1/caml/config.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/config.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h
 coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/alloc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h \
   kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/alloc.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h
 coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/compatibility.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /home/logical/local//lib/ocaml/caml/config.h \
-  /home/logical/local//lib/ocaml/caml/fail.h \
-  /home/logical/local//lib/ocaml/caml/mlvalues.h \
-  /home/logical/local//lib/ocaml/caml/misc.h \
-  /home/logical/local//lib/ocaml/caml/memory.h \
-  kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h
+  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+  /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_values.h \
+  /usr/lib/ocaml/3.09.1/caml/alloc.h