Ajout de l'axiome du but prouve par la tactique simplifi

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

7 files changed, 262 insertions, 192 deletions

diff --git a/.depend b/.depend
index e7a2efbe97..36f5d84107 100644
--- a/.depend
+++ b/.depend
@@ -53,12 +53,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/reduction.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \
     kernel/environ.cmi 
@@ -82,9 +82,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/entries.cmi kernel/declarations.cmi \
@@ -115,6 +112,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/ast.cmi: lib/util.cmi interp/topconstr.cmi lib/pp.cmi \
     kernel/names.cmi kernel/mod_subst.cmi library/libnames.cmi \
     interp/genarg.cmi lib/dyn.cmi parsing/coqast.cmi 
@@ -347,11 +347,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 
 translate/ppconstrnew.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \
     proofs/tacexpr.cmo pretyping/rawterm.cmi interp/ppextend.cmi lib/pp.cmi \
     parsing/pcoq.cmi pretyping/pattern.cmi kernel/names.cmi \
@@ -370,9 +370,9 @@ contrib/cc/ccalgo.cmi: kernel/term.cmi kernel/names.cmi
 contrib/cc/ccproof.cmi: kernel/names.cmi contrib/cc/ccalgo.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 \
@@ -506,6 +506,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 \
@@ -530,14 +538,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 
@@ -718,6 +718,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/cbytegen.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/cbytegen.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 \
@@ -732,14 +740,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/cbytegen.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/cbytegen.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/cbytegen.cmx kernel/modops.cmi 
 kernel/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/options.cmi \
     lib/hashcons.cmi kernel/names.cmi 
 kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/options.cmx \
@@ -834,10 +834,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 
@@ -846,24 +846,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/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 \
@@ -978,6 +968,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 parsing/ast.cmi 
@@ -2334,20 +2334,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 proofs/tacmach.cmi \
-    tactics/tacinterp.cmi lib/system.cmi library/states.cmi \
-    proofs/refiner.cmi translate/ppvernacnew.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 parsing/coqast.cmi \
-    interp/constrintern.cmi interp/constrextern.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
-    toplevel/vernacentries.cmx lib/util.cmx proofs/tacmach.cmx \
-    tactics/tacinterp.cmx lib/system.cmx library/states.cmx \
-    proofs/refiner.cmx translate/ppvernacnew.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 parsing/coqast.cmx \
-    interp/constrintern.cmx interp/constrextern.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 kernel/term.cmi \
@@ -2410,6 +2396,20 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \
     parsing/extend.cmx parsing/coqast.cmx parsing/ast.cmx \
     toplevel/vernacinterp.cmi 
+toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacentries.cmi lib/util.cmi proofs/tacmach.cmi \
+    tactics/tacinterp.cmi lib/system.cmi library/states.cmi \
+    proofs/refiner.cmi translate/ppvernacnew.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 parsing/coqast.cmi \
+    interp/constrintern.cmi interp/constrextern.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacentries.cmx lib/util.cmx proofs/tacmach.cmx \
+    tactics/tacinterp.cmx lib/system.cmx library/states.cmx \
+    proofs/refiner.cmx translate/ppvernacnew.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 parsing/coqast.cmx \
+    interp/constrintern.cmx interp/constrextern.cmx toplevel/vernac.cmi 
 translate/ppconstrnew.cmo: lib/util.cmi kernel/univ.cmi interp/topconstr.cmi \
     pretyping/termops.cmi kernel/term.cmi interp/syntax_def.cmi \
     pretyping/retyping.cmi pretyping/rawterm.cmi pretyping/pretyping.cmi \
@@ -2498,6 +2498,12 @@ contrib/cc/cctac.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
     pretyping/evd.cmx parsing/egrammar.cmx kernel/declarations.cmx \
     interp/coqlib.cmx toplevel/cerrors.cmx contrib/cc/ccproof.cmx \
     contrib/cc/ccalgo.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 \
@@ -2512,12 +2518,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 
@@ -2640,23 +2640,25 @@ 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.cmo: lib/util.cmi kernel/term.cmi tactics/tacticals.cmi \
-    proofs/tacmach.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \
-    contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi interp/coqlib.cmi \
-    contrib/dp/dp.cmi 
-contrib/dp/dp.cmx: lib/util.cmx kernel/term.cmx tactics/tacticals.cmx \
-    proofs/tacmach.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \
-    contrib/dp/fol.cmi contrib/dp/dp_simplify.cmx interp/coqlib.cmx \
-    contrib/dp/dp.cmi 
+contrib/dp/dp.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
+    tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi lib/pp.cmi \
+    library/nametab.cmi kernel/names.cmi library/nameops.cmi \
+    library/libnames.cmi tactics/hipattern.cmi contrib/dp/fol.cmi \
+    contrib/dp/dp_simplify.cmi interp/coqlib.cmi contrib/dp/dp.cmi 
+contrib/dp/dp.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
+    tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx lib/pp.cmx \
+    library/nametab.cmx kernel/names.cmx library/nameops.cmx \
+    library/libnames.cmx tactics/hipattern.cmx contrib/dp/fol.cmi \
+    contrib/dp/dp_simplify.cmx interp/coqlib.cmx contrib/dp/dp.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/g_dp.cmo: lib/util.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
-    proofs/refiner.cmi parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi \
-    lib/options.cmi parsing/egrammar.cmi contrib/dp/dp.cmi \
+contrib/dp/g_dp.cmo: lib/util.cmi tactics/tactics.cmi tactics/tacinterp.cmi \
+    proofs/tacexpr.cmo proofs/refiner.cmi parsing/pptactic.cmi lib/pp.cmi \
+    parsing/pcoq.cmi lib/options.cmi parsing/egrammar.cmi contrib/dp/dp.cmi \
     toplevel/cerrors.cmi 
-contrib/dp/g_dp.cmx: lib/util.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
-    proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \
-    lib/options.cmx parsing/egrammar.cmx contrib/dp/dp.cmx \
+contrib/dp/g_dp.cmx: lib/util.cmx tactics/tactics.cmx tactics/tacinterp.cmx \
+    proofs/tacexpr.cmx proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx \
+    parsing/pcoq.cmx lib/options.cmx parsing/egrammar.cmx contrib/dp/dp.cmx \
     toplevel/cerrors.cmx 
 contrib/extraction/common.cmo: lib/util.cmi kernel/term.cmi \
     contrib/extraction/table.cmi contrib/extraction/scheme.cmi \
@@ -3124,6 +3126,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 \
+    parsing/esyntax.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 \
+    parsing/esyntax.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 parsing/termast.cmi kernel/term.cmi \
@@ -3148,14 +3158,6 @@ contrib/interface/showproof.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     pretyping/evd.cmx kernel/environ.cmx kernel/declarations.cmx \
     parsing/coqast.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 \
-    parsing/esyntax.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 \
-    parsing/esyntax.cmx contrib/interface/ascent.cmi 
 contrib/interface/translate.cmo: contrib/interface/xlate.cmi \
     contrib/interface/vtp.cmi toplevel/vernacinterp.cmi lib/util.cmi \
     parsing/termast.cmi kernel/term.cmi proofs/tacmach.cmi kernel/sign.cmi \
@@ -3336,18 +3338,12 @@ contrib/romega/refl_omega.cmx: lib/util.cmx kernel/term.cmx \
     parsing/printer.cmx lib/pp.cmx lib/options.cmx contrib/omega/omega.cmx \
     kernel/names.cmx proofs/logic.cmx interp/coqlib.cmx \
     contrib/romega/const_omega.cmx lib/bigint.cmx 
-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 \
@@ -3366,6 +3362,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 \
@@ -3408,8 +3410,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 \
     kernel/sign.cmi pretyping/recordops.cmi proofs/proof_trees.cmi \
@@ -3440,10 +3440,8 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \
     toplevel/vernacinterp.cmx lib/util.cmx lib/pp.cmx parsing/pcoq.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 
@@ -3454,6 +3452,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 \
@@ -3583,72 +3585,58 @@ 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/mlvalues.h \
-  /home/logical/local/lib/ocaml/caml/fail.h \
-  /home/logical/local/lib/ocaml/caml/memory.h \
+  /usr/lib/ocaml/3.08/caml/config.h \
+  /usr/lib/ocaml/3.08/caml/compatibility.h \
+  /usr/lib/ocaml/3.08/caml/misc.h /usr/lib/ocaml/3.08/caml/mlvalues.h \
+  /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \
-  /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
-  kernel/byterun/coq_jumptbl.h
+  /usr/lib/ocaml/3.08/caml/mlvalues.h \
+  /usr/lib/ocaml/3.08/caml/compatibility.h \
+  /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \
+  /usr/lib/ocaml/3.08/caml/alloc.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \
-  /home/logical/local/lib/ocaml/caml/memory.h
+  /usr/lib/ocaml/3.08/caml/mlvalues.h \
+  /usr/lib/ocaml/3.08/caml/compatibility.h \
+  /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \
+  /usr/lib/ocaml/3.08/caml/alloc.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.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.08/caml/mlvalues.h \
+  /usr/lib/ocaml/3.08/caml/compatibility.h \
+  /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/caml/memory.h \
+  kernel/byterun/coq_values.h /usr/lib/ocaml/3.08/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/mlvalues.h \
-  /home/logical/local/lib/ocaml/caml/fail.h \
-  /home/logical/local/lib/ocaml/caml/memory.h \
+  /usr/lib/ocaml/3.08/caml/config.h \
+  /usr/lib/ocaml/3.08/caml/compatibility.h \
+  /usr/lib/ocaml/3.08/caml/misc.h /usr/lib/ocaml/3.08/caml/mlvalues.h \
+  /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \
-  /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
-  kernel/byterun/coq_jumptbl.h
+  /usr/lib/ocaml/3.08/caml/mlvalues.h \
+  /usr/lib/ocaml/3.08/caml/compatibility.h \
+  /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \
+  /usr/lib/ocaml/3.08/caml/alloc.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \
-  /home/logical/local/lib/ocaml/caml/memory.h
+  /usr/lib/ocaml/3.08/caml/mlvalues.h \
+  /usr/lib/ocaml/3.08/caml/compatibility.h \
+  /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \
+  /usr/lib/ocaml/3.08/caml/alloc.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.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.08/caml/mlvalues.h \
+  /usr/lib/ocaml/3.08/caml/compatibility.h \
+  /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/caml/memory.h \
+  kernel/byterun/coq_values.h /usr/lib/ocaml/3.08/caml/alloc.h
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 417d74b6df..6e9fdac6ee 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -9,7 +9,9 @@ open Tacmach
 open Fol
 open Names
 open Nameops
+open Termops
 open Coqlib
+open Hipattern
 
 let logic_dir = ["Coq";"Logic";"Decidable"]
 let coq_modules =
@@ -19,6 +21,16 @@ let coq_modules =
 let constant = gen_constant_in_modules "Omega" coq_modules
 
 let coq_Z = lazy (constant "Z")
+let coq_Zplus = lazy (constant "Zplus")
+let coq_Zmult = lazy (constant "Zmult")
+let coq_Zopp = lazy (constant "Zopp")
+let coq_Zminus = lazy (constant "Zminus")
+let coq_Zdiv = lazy (constant "Zdiv")
+let coq_Zs = lazy (constant "Zs")
+let coq_Zgt = lazy (constant "Zgt")
+let coq_Zle = lazy (constant "Zle")
+let coq_Zge = lazy (constant "Zge")
+let coq_Zlt = lazy (constant "Zlt")
 
 (* not Prop typed expressions *)
 exception NotProp
@@ -27,23 +39,70 @@ exception NotProp
 exception NotFO
 
 (* assumption: t:Set *)
-let tr_type env t =
+let rec tr_type env t =
   if t = Lazy.force coq_Z then Base "INT"
+  else if is_Prop t then Base "BOOLEAN"
+  else if is_Set t then Base "TYPE"
+  else if is_imp_term t then 
+    begin match match_with_imp_term t with
+      | Some (t1, t2) -> Arrow (tr_type env t1, tr_type env t2)
+      | _ -> assert false
+    end
+  (* else if then *)
   else raise NotFO
 
 (* assumption: t:T:Set *)
-let tr_term env t =
+let rec tr_term env t =
   match kind_of_term t with
-    | Var id -> Tvar (string_of_id id)
-    | _ -> raise NotFO
+    | Var id -> 
+	Tvar (string_of_id id)
+    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> 
+	Plus (tr_term env a, tr_term env b)
+    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> 
+	Moins (tr_term env a, tr_term env b)
+    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> 
+	Mult (tr_term env a, tr_term env b)
+    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> 
+	Div (tr_term env a, tr_term env b)
+    | Term.App (f, cl) -> 
+	begin try
+	  let r = Libnames.reference_of_constr f in
+	  let s = string_of_id (Nametab.id_of_global r) in
+	  App (s, List.map (tr_term env) (Array.to_list cl))
+	with Not_found ->
+	  raise NotFO
+	end
+    | _ -> 
+	raise NotFO
 
 (* assumption: f is of type Prop *)
-let tr_formula env f =
+let rec tr_formula env f =
   let c, args = decompose_app f in
   match kind_of_term c, args with
+    | Var id, [] -> 
+	Fvar (string_of_id id)
     | _, [t;a;b] when c = build_coq_eq () -> 
 	(* TODO: verifier type t *)
 	Fatom (Eq (tr_term env a, tr_term env b))
+    | _, [a;b] when c = Lazy.force coq_Zle ->
+	Fatom (Le (tr_term env a, tr_term env b))
+    | _, [] when c = build_coq_False () ->
+	False
+    | _, [] when c = build_coq_True () ->
+	True
+    | _, [a] when c = build_coq_not () ->
+	Not (tr_formula env a)
+    | _, [a;b] when c = build_coq_and () ->
+	And (tr_formula env a, tr_formula env b)
+    | _, [a;b] when c = build_coq_or () ->
+	Or (tr_formula env a, tr_formula env b)
+    | Prod (_, a, b), _ ->
+	if is_imp_term f then
+	  Imp (tr_formula env a, tr_formula env b)
+	else
+	  assert false (*TODO Forall *)
+    | _, [a] when c = build_coq_ex () ->
+	assert false (*TODO*) (*Exists (tr_formula env a)*)
     | _ ->
 	raise NotFO
 
@@ -73,18 +132,11 @@ let tr_goal gl =
   hyps, c
 
 
-(* Checks if a Coq formula is first-ordered *) 
-let rec is_FO c = match kind_of_term c with
-    Prod(n, t1, t2) -> assert false (*TODO*)
-  | Lambda(n, t, c) ->assert false (*TODO*)
-  | _ -> false
-
-(* Translates a first-order Coq formula into a specific first-order
- language formula *)
-(* let rec to_FO f = *)
-
 let rec isGoodType gl t = 
-(is_Prop t) || (is_Set t) || (is_Prop (pf_type_of gl (body_of_type t))) || (is_Set (pf_type_of gl (body_of_type t)))
+  (is_Prop t) || 
+  (is_Set t) || 
+  (is_Prop (pf_type_of gl (body_of_type t))) || 
+  (is_Set (pf_type_of gl (body_of_type t)))
 
 
 let rec allGoodTypeHyps gl hyps_types = match hyps_types with
@@ -103,18 +155,6 @@ let allGoodType gl =
   let hyps_types = pf_hyps_types gl in 
   allGoodTypeHyps gl hyps_types
 
-(*** UTILISER prterm
-let rec type_to_string t = match kind_of_term t with
-    Sort (Prop Null) -> "Prop "
-  | Sort (Prop Pos) -> "Set "
-  | Sort (Type _) -> "Type "
-  | Cast (c,_) -> type_to_string c
-  | _ -> "Other"
-
-let rec hyps_types_to_string = function
-    [] -> ""
-  | e::l -> (type_to_string e) ^ (hyps_types_to_string l)
-***)
 
 type prover = Simplify | CVCLite | Harvey
 
@@ -122,10 +162,6 @@ let call_prover prover q = match prover with
   | Simplify -> Dp_simplify.call q
   | CVCLite -> error "CVC Lite not yet interfaced"
   | Harvey -> error "haRVey not yet interfaced"
-
-let admit_as_an_axiom gl =
-  msgnl (str "Valid!");
-  Tacticals.tclIDTAC gl
   
 let dp prover gl =
   let concl_type = pf_type_of gl (pf_concl gl) in
@@ -133,7 +169,7 @@ let dp prover gl =
   try 
     let q = tr_goal gl in
     begin match call_prover prover q with
-      | Valid -> admit_as_an_axiom gl
+      | Valid -> Tactics.admit_as_an_axiom gl
       | Invalid -> error "Invalid"
       | DontKnow -> error "Don't know"
       | Timeout -> error "Timeout"
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
index da32e50662..40a5230894 100644
--- a/contrib/dp/dp.mli
+++ b/contrib/dp/dp.mli
@@ -2,3 +2,4 @@
 open Proof_type
 
 val simplify : tactic
+
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
index de5d898793..35370c6fdc 100644
--- a/contrib/dp/dp_simplify.ml
+++ b/contrib/dp/dp_simplify.ml
@@ -14,8 +14,14 @@ let rec print_term fmt = function
       fprintf fmt "%s" id
   | Cst n -> 
       fprintf fmt "%d" n
-  | Plus _ | Moins _ | Div _ | Mult _ ->
-      assert false (*TODO*) (* (+ a b) *)
+  | Plus (a, b) ->
+      fprintf fmt "@[(+@ %a@ %a)@]" print_term a print_term b
+  | Moins (a, b) ->
+      fprintf fmt "@[(-@ %a@ %a)@]" print_term a print_term b
+  | Mult (a, b) ->
+      fprintf fmt "@[(*@ %a@ %a)@]" (**) print_term a print_term b
+  | Div (a, b) ->
+      fprintf fmt "@[(/@ %a@ %a)@]" print_term a print_term b
   | App (id, []) ->
       fprintf fmt "%s" id 
   | App (id, tl) ->
@@ -38,11 +44,15 @@ let rec print_predicate fmt p =
   | Fatom (Eq (a, b)) ->
       fprintf fmt "@[(EQ %a@ %a)@]" print_term a print_term b
   | Fatom (Le (a, b)) ->
-      fprintf fmt "@[(<= %a %a)@]" print_term a print_term b
+      fprintf fmt "@[(<= %a@ %a)@]" print_term a print_term b
+  | Fatom (Lt (a, b))->
+      fprintf fmt "@[(< %a@ %a)@]" print_term a print_term b
+  | Fatom (Ge (a, b)) ->
+      fprintf fmt "@[(>= %a@ %a)@]" print_term a print_term b
+  | Fatom (Gt (a, b)) ->
+      fprintf fmt "@[(> %a@ %a)@]" print_term a print_term b
   | Fatom (Pred (id, tl)) -> 
       fprintf fmt "@[(EQ (%s@ %a) |@@true|)@]" id print_terms tl
-  | Fatom _ ->
-      assert false (*TODO*)
   | Imp (a, b) ->
       fprintf fmt "@[(IMPLIES@ %a@ %a)@]" pp a pp b
   | And (a, b) ->
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index 607b4d9cc0..6a984dda30 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -16,3 +16,7 @@ TACTIC EXTEND Simplify
   [ "simplify" ] -> [ simplify ]
 END
 
+(* should be part of basic tactics syntax *)
+TACTIC EXTEND admit
+  [ "admit"    ] -> [ Tactics.admit_as_an_axiom ]
+END
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5c0ed93575..198a17bcd9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1910,3 +1910,32 @@ let tclABSTRACT name_op tac gls =
     | None   -> add_suffix (get_current_proof_name ()) "_subproof" 
   in  
   abstract_subproof s tac gls
+
+
+let admit_as_an_axiom gls =
+  let env = Global.env() in
+  let current_sign = Global.named_context()
+  and global_sign = pf_hyps gls in
+  let sign,secsign = 
+    List.fold_right
+      (fun (id,_,_ as d) (s1,s2) -> 
+	 if mem_named_context id current_sign &
+           interpretable_as_section_decl (Sign.lookup_named id current_sign) d
+         then (s1,add_named_decl d s2)
+	 else (add_named_decl d s1,s2)) 
+      global_sign (empty_named_context,empty_named_context) in
+  let name = add_suffix (get_current_proof_name ()) "_admitted" in
+  let na = next_global_ident_away false name (pf_ids_of_hyps gls) in
+  let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in
+  if occur_existential concl then
+    if !Options.v7 then error "admit cannot handle existentials"
+    else error "\"admit\" cannot handle existentials";
+  let axiom =
+    let cd = Entries.ParameterEntry concl in
+    let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in
+    constr_of_global (ConstRef con)
+  in
+  exact_no_check 
+    (applist (axiom, 
+              List.rev (Array.to_list (instance_from_named_context sign))))
+    gls
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 34c4e6397b..5b03a79dd7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -248,3 +248,5 @@ val generalize                  : constr list -> tactic
 val generalize_dep              : constr  -> tactic
 
 val tclABSTRACT : identifier option -> tactic -> tactic
+
+val admit_as_an_axiom : tactic