Romega/names/Makefile

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

8 files changed, 3138 insertions, 454 deletions

diff --git a/.depend b/.depend
index 416277e17..ad9eeb4a2 100644
--- a/.depend
+++ b/.depend
@@ -1,7 +1,7 @@
 kernel/closure.cmi: kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \
     kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 kernel/cooking.cmi: kernel/declarations.cmi kernel/environ.cmi \
-    kernel/names.cmi kernel/term.cmi 
+    kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/declarations.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
 kernel/environ.cmi: kernel/declarations.cmi kernel/names.cmi lib/pp.cmi \
@@ -34,7 +34,7 @@ lib/util.cmi: lib/pp.cmi
 library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
-    library/nametab.cmi kernel/sign.cmi kernel/term.cmi 
+    library/nametab.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 library/global.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi \
     library/nametab.cmi kernel/safe_typing.cmi kernel/sign.cmi \
@@ -50,43 +50,12 @@ library/library.cmi: library/lib.cmi library/libobject.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi lib/system.cmi 
 library/nametab.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi lib/util.cmi 
 library/summary.cmi: kernel/names.cmi 
-parsing-sans-slam/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
-    parsing/pcoq.cmi lib/pp.cmi 
-parsing-sans-slam/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi \
-    kernel/evd.cmi library/impargs.cmi kernel/names.cmi library/nametab.cmi \
-    pretyping/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \
-    kernel/term.cmi 
-parsing-sans-slam/coqast.cmi: lib/dyn.cmi kernel/names.cmi 
-parsing-sans-slam/coqlib.cmi: kernel/names.cmi pretyping/pattern.cmi \
-    kernel/term.cmi 
-parsing-sans-slam/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi \
-    parsing/extend.cmi parsing/pcoq.cmi 
-parsing-sans-slam/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi \
-    parsing/extend.cmi lib/pp.cmi 
-parsing-sans-slam/extend.cmi: parsing/ast.cmi parsing/coqast.cmi \
-    parsing/pcoq.cmi lib/pp.cmi 
-parsing-sans-slam/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/term.cmi 
-parsing-sans-slam/g_zsyntax.cmi: parsing/coqast.cmi 
-parsing-sans-slam/pcoq.cmi: parsing/coqast.cmi 
-parsing-sans-slam/prettyp.cmi: kernel/environ.cmi kernel/inductive.cmi \
-    library/lib.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    kernel/reduction.cmi kernel/safe_typing.cmi kernel/sign.cmi \
-    kernel/term.cmi 
-parsing-sans-slam/printer.cmi: parsing/coqast.cmi kernel/environ.cmi \
-    kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi pretyping/rawterm.cmi \
-    kernel/sign.cmi kernel/term.cmi 
-parsing-sans-slam/search.cmi: kernel/environ.cmi kernel/names.cmi \
-    pretyping/pattern.cmi lib/pp.cmi kernel/term.cmi 
-parsing-sans-slam/termast.cmi: parsing/coqast.cmi kernel/environ.cmi \
-    kernel/names.cmi library/nametab.cmi pretyping/pattern.cmi \
-    pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi 
-parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
-    library/impargs.cmi kernel/names.cmi library/nametab.cmi \
-    pretyping/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \
-    kernel/term.cmi 
+parsing/astterm.cmi: parsing/coqast.cmi kernel/declarations.cmi \
+    kernel/environ.cmi kernel/evd.cmi library/impargs.cmi kernel/names.cmi \
+    library/nametab.cmi pretyping/pattern.cmi pretyping/rawterm.cmi \
+    kernel/sign.cmi kernel/term.cmi 
 parsing/coqast.cmi: lib/dyn.cmi kernel/names.cmi 
 parsing/coqlib.cmi: kernel/names.cmi pretyping/pattern.cmi kernel/term.cmi 
 parsing/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
@@ -201,9 +170,10 @@ tactics/refine.cmi: pretyping/pretyping.cmi proofs/tacmach.cmi \
     kernel/term.cmi 
 tactics/setoid_replace.cmi: proofs/proof_type.cmi kernel/term.cmi 
 tactics/tacentries.cmi: proofs/proof_type.cmi proofs/tacmach.cmi 
-tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \
-    pretyping/pattern.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi 
+tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi \
+    kernel/declarations.cmi kernel/names.cmi pretyping/pattern.cmi \
+    proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \
+    proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi 
 tactics/tactics.cmi: proofs/clenv.cmi kernel/closure.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi kernel/evd.cmi kernel/names.cmi \
     proofs/proof_type.cmi kernel/reduction.cmi proofs/tacmach.cmi \
@@ -314,28 +284,6 @@ contrib/interface/translate.cmi: contrib/interface/ascent.cmi \
 contrib/interface/vtp.cmi: contrib/interface/ascent.cmi 
 contrib/interface/xlate.cmi: contrib/interface/ascent.cmi \
     contrib/interface/ctast.cmo 
-contrib/interface_essai/ascent.cmi: kernel/names.cmi 
-contrib/interface_essai/dad.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
-    proofs/tacmach.cmi 
-contrib/interface_essai/debug_tac.cmi: parsing/coqast.cmi \
-    proofs/proof_type.cmi proofs/tacmach.cmi 
-contrib/interface_essai/name_to_ast.cmi: parsing/coqast.cmi \
-    library/nametab.cmi 
-contrib/interface_essai/pbp.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
-    proofs/tacmach.cmi 
-contrib/interface_essai/showproof.cmi: contrib/interface/ascent.cmi \
-    parsing/astterm.cmi proofs/clenv.cmi parsing/coqast.cmi \
-    kernel/declarations.cmi kernel/environ.cmi kernel/evd.cmi \
-    kernel/inductive.cmi kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi \
-    parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
-    kernel/reduction.cmi contrib/interface/showproof_ct.cmo kernel/sign.cmi \
-    lib/stamps.cmi kernel/term.cmi contrib/interface/translate.cmi \
-    pretyping/typing.cmi lib/util.cmi toplevel/vernacinterp.cmi 
-contrib/interface_essai/translate.cmi: contrib/interface/ascent.cmi \
-    kernel/environ.cmi kernel/evd.cmi proofs/proof_type.cmi kernel/term.cmi 
-contrib/interface_essai/vtp.cmi: contrib/interface/ascent.cmi 
-contrib/interface_essai/xlate.cmi: contrib/interface/ascent.cmi \
-    parsing/coqast.cmi 
 contrib/xml/xmlcommand.cmi: kernel/names.cmi library/nametab.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
@@ -489,7 +437,7 @@ library/declare.cmo: kernel/cooking.cmi kernel/declarations.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi kernel/reduction.cmi \
     kernel/sign.cmi library/summary.cmi kernel/term.cmi \
-    kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
+    kernel/type_errors.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \
     library/declare.cmi 
 library/declare.cmx: kernel/cooking.cmx kernel/declarations.cmx \
     kernel/environ.cmx kernel/evd.cmx library/global.cmx library/impargs.cmx \
@@ -497,7 +445,7 @@ library/declare.cmx: kernel/cooking.cmx kernel/declarations.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx \
     library/nametab.cmx lib/options.cmx lib/pp.cmx kernel/reduction.cmx \
     kernel/sign.cmx library/summary.cmx kernel/term.cmx \
-    kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
+    kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
     library/declare.cmi 
 library/global.cmo: kernel/environ.cmi kernel/inductive.cmi \
     kernel/instantiate.cmi kernel/names.cmi library/nametab.cmi \
@@ -559,163 +507,27 @@ 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 
-parsing-sans-slam/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
-    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing-sans-slam/ast.cmi 
-parsing-sans-slam/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \
-    parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing-sans-slam/ast.cmi 
-parsing-sans-slam/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    library/declare.cmi kernel/environ.cmi pretyping/evarutil.cmi \
-    kernel/evd.cmi library/global.cmi library/impargs.cmi kernel/names.cmi \
-    library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
-    pretyping/pretype_errors.cmi pretyping/pretyping.cmi \
-    pretyping/rawterm.cmi kernel/reduction.cmi pretyping/retyping.cmi \
-    kernel/sign.cmi pretyping/syntax_def.cmi kernel/term.cmi \
-    parsing/termast.cmi pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \
-    parsing-sans-slam/astterm.cmi 
-parsing-sans-slam/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \
-    kernel/evd.cmx library/global.cmx library/impargs.cmx kernel/names.cmx \
-    library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
-    pretyping/pretype_errors.cmx pretyping/pretyping.cmx \
-    pretyping/rawterm.cmx kernel/reduction.cmx pretyping/retyping.cmx \
-    kernel/sign.cmx pretyping/syntax_def.cmx kernel/term.cmx \
-    parsing/termast.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \
-    parsing-sans-slam/astterm.cmi 
-parsing-sans-slam/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi kernel/names.cmi \
-    parsing-sans-slam/coqast.cmi 
-parsing-sans-slam/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx kernel/names.cmx \
-    parsing-sans-slam/coqast.cmi 
-parsing-sans-slam/coqlib.cmo: library/declare.cmi kernel/evd.cmi \
-    library/global.cmi kernel/names.cmi library/nametab.cmi \
-    pretyping/pattern.cmi kernel/term.cmi lib/util.cmi \
-    parsing-sans-slam/coqlib.cmi 
-parsing-sans-slam/coqlib.cmx: library/declare.cmx kernel/evd.cmx \
-    library/global.cmx kernel/names.cmx library/nametab.cmx \
-    pretyping/pattern.cmx kernel/term.cmx lib/util.cmx \
-    parsing-sans-slam/coqlib.cmi 
-parsing-sans-slam/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    parsing/extend.cmi parsing/lexer.cmi parsing/pcoq.cmi lib/pp.cmi \
-    lib/util.cmi parsing-sans-slam/egrammar.cmi 
-parsing-sans-slam/egrammar.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    parsing/extend.cmx parsing/lexer.cmx parsing/pcoq.cmx lib/pp.cmx \
-    lib/util.cmx parsing-sans-slam/egrammar.cmi 
-parsing-sans-slam/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    parsing/extend.cmi lib/gmap.cmi lib/gmapl.cmi kernel/names.cmi lib/pp.cmi \
-    lib/util.cmi parsing-sans-slam/esyntax.cmi 
-parsing-sans-slam/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    parsing/extend.cmx lib/gmap.cmx lib/gmapl.cmx kernel/names.cmx lib/pp.cmx \
-    lib/util.cmx parsing-sans-slam/esyntax.cmi 
-parsing-sans-slam/g_natsyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    parsing/coqlib.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \
-    lib/pp.cmi parsing/termast.cmi lib/util.cmi \
-    parsing-sans-slam/g_natsyntax.cmi 
-parsing-sans-slam/g_natsyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    parsing/coqlib.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx \
-    lib/pp.cmx parsing/termast.cmx lib/util.cmx \
-    parsing-sans-slam/g_natsyntax.cmi 
-parsing-sans-slam/g_rsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
-    parsing/coqast.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \
-    lib/pp.cmi lib/util.cmi 
-parsing-sans-slam/g_rsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
-    parsing/coqast.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx \
-    lib/pp.cmx lib/util.cmx 
-parsing-sans-slam/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
-    parsing/coqast.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \
-    lib/pp.cmi lib/util.cmi parsing-sans-slam/g_zsyntax.cmi 
-parsing-sans-slam/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
-    parsing/coqast.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx \
-    lib/pp.cmx lib/util.cmx parsing-sans-slam/g_zsyntax.cmi 
-parsing-sans-slam/pretty.cmo: pretyping/classops.cmi kernel/declarations.cmi \
-    library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
-    library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \
-    library/lib.cmi library/libobject.cmi library/library.cmi \
-    kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
-    kernel/reduction.cmi kernel/safe_typing.cmi kernel/sign.cmi \
-    pretyping/syntax_def.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi 
-parsing-sans-slam/pretty.cmx: pretyping/classops.cmx kernel/declarations.cmx \
-    library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
-    library/impargs.cmx kernel/inductive.cmx kernel/instantiate.cmx \
-    library/lib.cmx library/libobject.cmx library/library.cmx \
-    kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
-    kernel/reduction.cmx kernel/safe_typing.cmx kernel/sign.cmx \
-    pretyping/syntax_def.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx 
-parsing-sans-slam/prettyp.cmo: pretyping/classops.cmi kernel/declarations.cmi \
-    library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
-    library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \
-    library/lib.cmi library/libobject.cmi kernel/names.cmi \
-    library/nametab.cmi lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi \
-    kernel/safe_typing.cmi kernel/sign.cmi pretyping/syntax_def.cmi \
-    kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
-    parsing-sans-slam/prettyp.cmi 
-parsing-sans-slam/prettyp.cmx: pretyping/classops.cmx kernel/declarations.cmx \
-    library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
-    library/impargs.cmx kernel/inductive.cmx kernel/instantiate.cmx \
-    library/lib.cmx library/libobject.cmx kernel/names.cmx \
-    library/nametab.cmx lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx \
-    kernel/safe_typing.cmx kernel/sign.cmx pretyping/syntax_def.cmx \
-    kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
-    parsing-sans-slam/prettyp.cmi 
-parsing-sans-slam/printer.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    library/declare.cmi kernel/environ.cmi parsing/esyntax.cmi \
-    parsing/extend.cmi library/global.cmi kernel/names.cmi lib/options.cmi \
-    pretyping/pattern.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \
-    parsing/termast.cmi lib/util.cmi parsing-sans-slam/printer.cmi 
-parsing-sans-slam/printer.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    library/declare.cmx kernel/environ.cmx parsing/esyntax.cmx \
-    parsing/extend.cmx library/global.cmx kernel/names.cmx lib/options.cmx \
-    pretyping/pattern.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \
-    parsing/termast.cmx lib/util.cmx parsing-sans-slam/printer.cmi 
-parsing-sans-slam/search.cmo: parsing/astterm.cmi parsing/coqast.cmi \
-    parsing/coqlib.cmi kernel/declarations.cmi library/declare.cmi \
-    kernel/environ.cmi kernel/evd.cmi library/global.cmi \
-    library/libobject.cmi library/library.cmi kernel/names.cmi \
-    pretyping/pattern.cmi lib/pp.cmi pretyping/pretyping.cmi \
-    parsing/printer.cmi pretyping/rawterm.cmi pretyping/retyping.cmi \
-    kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
-    parsing-sans-slam/search.cmi 
-parsing-sans-slam/search.cmx: parsing/astterm.cmx parsing/coqast.cmx \
-    parsing/coqlib.cmx kernel/declarations.cmx library/declare.cmx \
-    kernel/environ.cmx kernel/evd.cmx library/global.cmx \
-    library/libobject.cmx library/library.cmx kernel/names.cmx \
-    pretyping/pattern.cmx lib/pp.cmx pretyping/pretyping.cmx \
-    parsing/printer.cmx pretyping/rawterm.cmx pretyping/retyping.cmx \
-    kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
-    parsing-sans-slam/search.cmi 
-parsing-sans-slam/termast.cmo: parsing/ast.cmi pretyping/classops.cmi \
-    parsing/coqast.cmi library/declare.cmi pretyping/detyping.cmi \
-    kernel/environ.cmi library/impargs.cmi kernel/inductive.cmi \
-    kernel/names.cmi library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
-    pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/univ.cmi lib/util.cmi \
-    parsing-sans-slam/termast.cmi 
-parsing-sans-slam/termast.cmx: parsing/ast.cmx pretyping/classops.cmx \
-    parsing/coqast.cmx library/declare.cmx pretyping/detyping.cmx \
-    kernel/environ.cmx library/impargs.cmx kernel/inductive.cmx \
-    kernel/names.cmx library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
-    pretyping/rawterm.cmx kernel/reduction.cmx kernel/sign.cmx \
-    kernel/term.cmx kernel/univ.cmx lib/util.cmx \
-    parsing-sans-slam/termast.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 \
     parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/ast.cmi 
-parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
-    kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
-    library/global.cmi library/impargs.cmi kernel/names.cmi \
-    library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
-    pretyping/pretype_errors.cmi pretyping/pretyping.cmi \
-    pretyping/rawterm.cmi kernel/reduction.cmi pretyping/retyping.cmi \
-    kernel/sign.cmi pretyping/syntax_def.cmi kernel/term.cmi \
-    parsing/termast.cmi pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \
+parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi \
+    kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
+    pretyping/evarutil.cmi kernel/evd.cmi library/global.cmi \
+    library/impargs.cmi kernel/names.cmi library/nametab.cmi \
+    pretyping/pattern.cmi lib/pp.cmi pretyping/pretype_errors.cmi \
+    pretyping/pretyping.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
+    pretyping/retyping.cmi kernel/sign.cmi pretyping/syntax_def.cmi \
+    kernel/term.cmi parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \
     parsing/astterm.cmi 
-parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
-    kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \
-    library/global.cmx library/impargs.cmx kernel/names.cmx \
-    library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
-    pretyping/pretype_errors.cmx pretyping/pretyping.cmx \
-    pretyping/rawterm.cmx kernel/reduction.cmx pretyping/retyping.cmx \
-    kernel/sign.cmx pretyping/syntax_def.cmx kernel/term.cmx \
-    parsing/termast.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \
+parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx \
+    kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
+    pretyping/evarutil.cmx kernel/evd.cmx library/global.cmx \
+    library/impargs.cmx kernel/names.cmx library/nametab.cmx \
+    pretyping/pattern.cmx lib/pp.cmx pretyping/pretype_errors.cmx \
+    pretyping/pretyping.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
+    pretyping/retyping.cmx kernel/sign.cmx pretyping/syntax_def.cmx \
+    kernel/term.cmx parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \
     parsing/astterm.cmi 
 parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi kernel/names.cmi \
     parsing/coqast.cmi 
@@ -799,20 +611,6 @@ parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
     lib/util.cmi parsing/pcoq.cmi 
 parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
     lib/util.cmx parsing/pcoq.cmi 
-parsing/pretty.cmo: pretyping/classops.cmi kernel/declarations.cmi \
-    library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
-    library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \
-    library/lib.cmi library/libobject.cmi library/library.cmi \
-    kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
-    kernel/reduction.cmi kernel/safe_typing.cmi kernel/sign.cmi \
-    pretyping/syntax_def.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi 
-parsing/pretty.cmx: pretyping/classops.cmx kernel/declarations.cmx \
-    library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
-    library/impargs.cmx kernel/inductive.cmx kernel/instantiate.cmx \
-    library/lib.cmx library/libobject.cmx library/library.cmx \
-    kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
-    kernel/reduction.cmx kernel/safe_typing.cmx kernel/sign.cmx \
-    pretyping/syntax_def.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx 
 parsing/prettyp.cmo: pretyping/classops.cmi kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
     library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \
@@ -870,14 +668,14 @@ pretyping/cases.cmo: pretyping/coercion.cmi kernel/declarations.cmi \
     library/global.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/pretype_errors.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
     pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/type_errors.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \
+    kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
     pretyping/cases.cmi 
 pretyping/cases.cmx: pretyping/coercion.cmx kernel/declarations.cmx \
     kernel/environ.cmx pretyping/evarconv.cmx pretyping/evarutil.cmx \
     library/global.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
     pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.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 kernel/evd.cmi \
@@ -930,11 +728,13 @@ pretyping/evarconv.cmx: pretyping/classops.cmx kernel/closure.cmx \
 pretyping/evarutil.cmo: kernel/environ.cmi kernel/evd.cmi library/global.cmi \
     library/indrec.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/pretype_errors.cmi kernel/reduction.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/univ.cmi lib/util.cmi pretyping/evarutil.cmi 
+    kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \
+    pretyping/evarutil.cmi 
 pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx library/global.cmx \
     library/indrec.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx kernel/reduction.cmx kernel/sign.cmx \
-    kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/evarutil.cmi 
+    kernel/term.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
+    pretyping/evarutil.cmi 
 pretyping/pattern.cmo: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
     library/global.cmi kernel/names.cmi pretyping/rawterm.cmi \
     kernel/reduction.cmi kernel/term.cmi lib/util.cmi pretyping/pattern.cmi 
@@ -956,7 +756,7 @@ pretyping/pretyping.cmo: pretyping/cases.cmi pretyping/classops.cmi \
     kernel/names.cmi lib/pp.cmi pretyping/pretype_errors.cmi \
     pretyping/rawterm.cmi pretyping/recordops.cmi kernel/reduction.cmi \
     pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/type_errors.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \
+    kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
     pretyping/pretyping.cmi 
 pretyping/pretyping.cmx: pretyping/cases.cmx pretyping/classops.cmx \
     pretyping/coercion.cmx library/declare.cmx kernel/environ.cmx \
@@ -965,7 +765,7 @@ pretyping/pretyping.cmx: pretyping/cases.cmx pretyping/classops.cmx \
     kernel/names.cmx lib/pp.cmx pretyping/pretype_errors.cmx \
     pretyping/rawterm.cmx pretyping/recordops.cmx kernel/reduction.cmx \
     pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
+    kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
     pretyping/pretyping.cmi 
 pretyping/rawterm.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi lib/util.cmi pretyping/rawterm.cmi 
@@ -991,16 +791,14 @@ pretyping/syntax_def.cmo: library/lib.cmi library/libobject.cmi \
 pretyping/syntax_def.cmx: library/lib.cmx library/libobject.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 \
-    library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
-    kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
-    kernel/reduction.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
-    pretyping/tacred.cmi 
-pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx \
-    library/declare.cmx kernel/environ.cmx kernel/evd.cmx \
-    kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
-    kernel/reduction.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \
-    pretyping/tacred.cmi 
+pretyping/tacred.cmo: pretyping/cbv.cmi kernel/closure.cmi kernel/environ.cmi \
+    kernel/evd.cmi kernel/inductive.cmi kernel/instantiate.cmi \
+    kernel/names.cmi lib/pp.cmi kernel/reduction.cmi library/summary.cmi \
+    kernel/term.cmi lib/util.cmi pretyping/tacred.cmi 
+pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx kernel/environ.cmx \
+    kernel/evd.cmx kernel/inductive.cmx kernel/instantiate.cmx \
+    kernel/names.cmx lib/pp.cmx kernel/reduction.cmx library/summary.cmx \
+    kernel/term.cmx lib/util.cmx pretyping/tacred.cmi 
 pretyping/typing.cmo: kernel/environ.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
     kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi 
@@ -1221,9 +1019,10 @@ tactics/eqdecide.cmx: tactics/auto.cmx parsing/coqlib.cmx \
     tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
 tactics/equality.cmo: parsing/astterm.cmi proofs/clenv.cmi parsing/coqast.cmi \
     parsing/coqlib.cmi library/declare.cmi kernel/environ.cmi \
-    proofs/evar_refiner.cmi kernel/evd.cmi library/global.cmi lib/gmapl.cmi \
-    tactics/hipattern.cmi kernel/inductive.cmi kernel/instantiate.cmi \
-    library/lib.cmi library/libobject.cmi proofs/logic.cmi kernel/names.cmi \
+    proofs/evar_refiner.cmi pretyping/evarutil.cmi kernel/evd.cmi \
+    library/global.cmi lib/gmapl.cmi tactics/hipattern.cmi \
+    kernel/inductive.cmi kernel/instantiate.cmi library/lib.cmi \
+    library/libobject.cmi proofs/logic.cmi kernel/names.cmi \
     pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \
     kernel/reduction.cmi pretyping/retyping.cmi tactics/setoid_replace.cmi \
     proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
@@ -1232,9 +1031,10 @@ tactics/equality.cmo: parsing/astterm.cmi proofs/clenv.cmi parsing/coqast.cmi \
     toplevel/vernacinterp.cmi tactics/wcclausenv.cmi tactics/equality.cmi 
 tactics/equality.cmx: parsing/astterm.cmx proofs/clenv.cmx parsing/coqast.cmx \
     parsing/coqlib.cmx library/declare.cmx kernel/environ.cmx \
-    proofs/evar_refiner.cmx kernel/evd.cmx library/global.cmx lib/gmapl.cmx \
-    tactics/hipattern.cmx kernel/inductive.cmx kernel/instantiate.cmx \
-    library/lib.cmx library/libobject.cmx proofs/logic.cmx kernel/names.cmx \
+    proofs/evar_refiner.cmx pretyping/evarutil.cmx kernel/evd.cmx \
+    library/global.cmx lib/gmapl.cmx tactics/hipattern.cmx \
+    kernel/inductive.cmx kernel/instantiate.cmx library/lib.cmx \
+    library/libobject.cmx proofs/logic.cmx kernel/names.cmx \
     pretyping/pattern.cmx lib/pp.cmx proofs/proof_type.cmx \
     kernel/reduction.cmx pretyping/retyping.cmx tactics/setoid_replace.cmx \
     proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
@@ -1332,19 +1132,17 @@ tactics/tacentries.cmx: proofs/proof_trees.cmx proofs/tacmach.cmx \
 tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi library/global.cmi library/indrec.cmi \
-    kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi \
-    pretyping/pattern.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
-    lib/stamps.cmi proofs/tacinterp.cmi proofs/tacmach.cmi kernel/term.cmi \
-    parsing/termast.cmi lib/util.cmi tactics/wcclausenv.cmi \
-    tactics/tacticals.cmi 
+    kernel/inductive.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
+    kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi proofs/tacinterp.cmi \
+    proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \
+    tactics/wcclausenv.cmi tactics/tacticals.cmi 
 tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \
     kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
     proofs/evar_refiner.cmx library/global.cmx library/indrec.cmx \
-    kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx \
-    pretyping/pattern.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \
-    lib/stamps.cmx proofs/tacinterp.cmx proofs/tacmach.cmx kernel/term.cmx \
-    parsing/termast.cmx lib/util.cmx tactics/wcclausenv.cmx \
-    tactics/tacticals.cmi 
+    kernel/inductive.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
+    kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \
+    proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
+    tactics/wcclausenv.cmx tactics/tacticals.cmi 
 tactics/tactics.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/closure.cmi \
     parsing/coqlib.cmi kernel/declarations.cmi library/declare.cmi \
     kernel/environ.cmi proofs/evar_refiner.cmi kernel/evd.cmi \
@@ -1446,8 +1244,8 @@ toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi toplevel/recordobj.cmi \
     pretyping/recordops.cmi kernel/reduction.cmi kernel/sign.cmi \
-    library/summary.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
-    toplevel/discharge.cmi 
+    library/summary.cmi kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi \
+    lib/util.cmi toplevel/discharge.cmi 
 toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \
     kernel/cooking.cmx kernel/declarations.cmx library/declare.cmx \
     kernel/environ.cmx library/global.cmx library/impargs.cmx \
@@ -1455,8 +1253,8 @@ toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx \
     library/nametab.cmx lib/options.cmx lib/pp.cmx toplevel/recordobj.cmx \
     pretyping/recordops.cmx kernel/reduction.cmx kernel/sign.cmx \
-    library/summary.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
-    toplevel/discharge.cmi 
+    library/summary.cmx kernel/term.cmx kernel/typeops.cmx kernel/univ.cmx \
+    lib/util.cmx toplevel/discharge.cmi 
 toplevel/errors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
     kernel/indtypes.cmi parsing/lexer.cmi proofs/logic.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi \
@@ -2081,196 +1879,22 @@ contrib/interface/xlate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
 contrib/interface/xlate.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \
     contrib/interface/ctast.cmx kernel/names.cmx lib/util.cmx \
     contrib/interface/xlate.cmi 
-contrib/interface_essai/centaur.cmo: contrib/interface/ascent.cmi \
-    parsing/ast.cmi parsing/astterm.cmi pretyping/classops.cmi \
-    toplevel/command.cmi parsing/coqast.cmi contrib/interface/dad.cmi \
-    contrib/interface/debug_tac.cmi kernel/declarations.cmi \
-    library/declare.cmi kernel/environ.cmi toplevel/errors.cmi kernel/evd.cmi \
-    library/global.cmi contrib/interface/history.cmi library/lib.cmi \
-    library/libobject.cmi library/library.cmi \
-    toplevel/line_oriented_parser.cmi toplevel/mltop.cmi \
-    contrib/interface/name_to_ast.cmi kernel/names.cmi library/nametab.cmi \
-    contrib/interface/pbp.cmi proofs/pfedit.cmi lib/pp.cmi \
-    pretyping/pretyping.cmi parsing/printer.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi toplevel/protectedtoplevel.cmi \
-    pretyping/rawterm.cmi kernel/reduction.cmi parsing/search.cmi \
-    contrib/interface/showproof.cmi contrib/interface/showproof_ct.cmo \
-    proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
-    kernel/term.cmi parsing/termast.cmi contrib/interface/translate.cmi \
-    lib/util.cmi toplevel/vernac.cmi toplevel/vernacentries.cmi \
-    toplevel/vernacinterp.cmi contrib/interface/vtp.cmi \
-    contrib/interface/xlate.cmi 
-contrib/interface_essai/centaur.cmx: contrib/interface/ascent.cmi \
-    parsing/ast.cmx parsing/astterm.cmx pretyping/classops.cmx \
-    toplevel/command.cmx parsing/coqast.cmx contrib/interface/dad.cmx \
-    contrib/interface/debug_tac.cmx kernel/declarations.cmx \
-    library/declare.cmx kernel/environ.cmx toplevel/errors.cmx kernel/evd.cmx \
-    library/global.cmx contrib/interface/history.cmx library/lib.cmx \
-    library/libobject.cmx library/library.cmx \
-    toplevel/line_oriented_parser.cmx toplevel/mltop.cmx \
-    contrib/interface/name_to_ast.cmx kernel/names.cmx library/nametab.cmx \
-    contrib/interface/pbp.cmx proofs/pfedit.cmx lib/pp.cmx \
-    pretyping/pretyping.cmx parsing/printer.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx toplevel/protectedtoplevel.cmx \
-    pretyping/rawterm.cmx kernel/reduction.cmx parsing/search.cmx \
-    contrib/interface/showproof.cmx contrib/interface/showproof_ct.cmx \
-    proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
-    kernel/term.cmx parsing/termast.cmx contrib/interface/translate.cmx \
-    lib/util.cmx toplevel/vernac.cmx toplevel/vernacentries.cmx \
-    toplevel/vernacinterp.cmx contrib/interface/vtp.cmx \
-    contrib/interface/xlate.cmx 
-contrib/interface_essai/dad.cmo: parsing/astterm.cmi parsing/coqast.cmi \
-    kernel/environ.cmi kernel/evd.cmi library/global.cmi kernel/names.cmi \
-    contrib/interface/paths.cmi pretyping/pattern.cmi lib/pp.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
-    kernel/reduction.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi \
-    pretyping/typing.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    contrib/interface_essai/dad.cmi 
-contrib/interface_essai/dad.cmx: parsing/astterm.cmx parsing/coqast.cmx \
-    kernel/environ.cmx kernel/evd.cmx library/global.cmx kernel/names.cmx \
-    contrib/interface/paths.cmx pretyping/pattern.cmx lib/pp.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
-    kernel/reduction.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \
-    pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    contrib/interface_essai/dad.cmi 
-contrib/interface_essai/debug_tac.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    toplevel/errors.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
-    lib/util.cmi contrib/interface_essai/debug_tac.cmi 
-contrib/interface_essai/debug_tac.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    toplevel/errors.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
-    lib/util.cmx contrib/interface_essai/debug_tac.cmi 
-contrib/interface_essai/history.cmo: contrib/interface/paths.cmi \
-    contrib/interface_essai/history.cmi 
-contrib/interface_essai/history.cmx: contrib/interface/paths.cmx \
-    contrib/interface_essai/history.cmi 
-contrib/interface_essai/line_parser.cmo: \
-    contrib/interface_essai/line_parser.cmi 
-contrib/interface_essai/line_parser.cmx: \
-    contrib/interface_essai/line_parser.cmi 
-contrib/interface_essai/name_to_ast.cmo: parsing/ast.cmi \
-    pretyping/classops.cmi parsing/coqast.cmi kernel/declarations.cmi \
-    library/declare.cmi kernel/environ.cmi library/global.cmi \
-    library/impargs.cmi kernel/inductive.cmi library/lib.cmi \
-    library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    parsing/prettyp.cmi kernel/reduction.cmi kernel/sign.cmi \
-    pretyping/syntax_def.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \
-    contrib/interface_essai/name_to_ast.cmi 
-contrib/interface_essai/name_to_ast.cmx: parsing/ast.cmx \
-    pretyping/classops.cmx parsing/coqast.cmx kernel/declarations.cmx \
-    library/declare.cmx kernel/environ.cmx library/global.cmx \
-    library/impargs.cmx kernel/inductive.cmx library/lib.cmx \
-    library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    parsing/prettyp.cmx kernel/reduction.cmx kernel/sign.cmx \
-    pretyping/syntax_def.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
-    contrib/interface_essai/name_to_ast.cmi 
-contrib/interface_essai/parse.cmo: contrib/interface/ascent.cmi \
-    parsing/ast.cmi config/coq_config.cmi parsing/coqast.cmi \
-    toplevel/errors.cmi parsing/esyntax.cmi library/libobject.cmi \
-    library/library.cmi contrib/interface/line_parser.cmi \
-    toplevel/metasyntax.cmi library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi \
-    lib/system.cmi lib/util.cmi contrib/interface/vtp.cmi \
-    contrib/interface/xlate.cmi 
-contrib/interface_essai/parse.cmx: contrib/interface/ascent.cmi \
-    parsing/ast.cmx config/coq_config.cmx parsing/coqast.cmx \
-    toplevel/errors.cmx parsing/esyntax.cmx library/libobject.cmx \
-    library/library.cmx contrib/interface/line_parser.cmx \
-    toplevel/metasyntax.cmx library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx \
-    lib/system.cmx lib/util.cmx contrib/interface/vtp.cmx \
-    contrib/interface/xlate.cmx 
-contrib/interface_essai/paths.cmo: contrib/interface_essai/paths.cmi 
-contrib/interface_essai/paths.cmx: contrib/interface_essai/paths.cmi 
-contrib/interface_essai/pbp.cmo: parsing/coqast.cmi parsing/coqlib.cmi \
-    library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
-    tactics/hipattern.cmi proofs/logic.cmi kernel/names.cmi \
-    library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
-    pretyping/pretyping.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
-    pretyping/rawterm.cmi kernel/reduction.cmi proofs/tacinterp.cmi \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
-    kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
-    contrib/interface_essai/pbp.cmi 
-contrib/interface_essai/pbp.cmx: parsing/coqast.cmx parsing/coqlib.cmx \
-    library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
-    tactics/hipattern.cmx proofs/logic.cmx kernel/names.cmx \
-    library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
-    pretyping/pretyping.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
-    pretyping/rawterm.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_essai/pbp.cmi 
-contrib/interface_essai/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \
-    proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \
-    kernel/environ.cmi kernel/evd.cmi library/global.cmi kernel/inductive.cmi \
-    kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    contrib/interface/showproof_ct.cmo kernel/sign.cmi lib/stamps.cmi \
-    proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \
-    contrib/interface/translate.cmi pretyping/typing.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi contrib/interface_essai/showproof.cmi 
-contrib/interface_essai/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \
-    proofs/clenv.cmx parsing/coqast.cmx kernel/declarations.cmx \
-    kernel/environ.cmx kernel/evd.cmx library/global.cmx kernel/inductive.cmx \
-    kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \
-    contrib/interface/showproof_ct.cmx kernel/sign.cmx lib/stamps.cmx \
-    proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \
-    contrib/interface/translate.cmx pretyping/typing.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx contrib/interface_essai/showproof.cmi 
-contrib/interface_essai/showproof_ct.cmo: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi \
-    kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
-    contrib/interface/translate.cmi contrib/interface/vtp.cmi \
-    contrib/interface/xlate.cmi 
-contrib/interface_essai/showproof_ct.cmx: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx \
-    kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
-    contrib/interface/translate.cmx contrib/interface/vtp.cmx \
-    contrib/interface/xlate.cmx 
-contrib/interface_essai/translate.cmo: contrib/interface/ascent.cmi \
-    parsing/ast.cmi parsing/coqast.cmi kernel/environ.cmi \
-    pretyping/evarutil.cmi kernel/evd.cmi library/libobject.cmi \
-    library/library.cmi kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi \
-    proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
-    parsing/termast.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    contrib/interface/vtp.cmi contrib/interface/xlate.cmi \
-    contrib/interface_essai/translate.cmi 
-contrib/interface_essai/translate.cmx: contrib/interface/ascent.cmi \
-    parsing/ast.cmx parsing/coqast.cmx kernel/environ.cmx \
-    pretyping/evarutil.cmx kernel/evd.cmx library/libobject.cmx \
-    library/library.cmx kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx \
-    proofs/proof_type.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
-    parsing/termast.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    contrib/interface/vtp.cmx contrib/interface/xlate.cmx \
-    contrib/interface_essai/translate.cmi 
-contrib/interface_essai/vtp.cmo: contrib/interface/ascent.cmi \
-    kernel/names.cmi contrib/interface_essai/vtp.cmi 
-contrib/interface_essai/vtp.cmx: contrib/interface/ascent.cmi \
-    kernel/names.cmx contrib/interface_essai/vtp.cmi 
-contrib/interface_essai/xlate.cmo: contrib/interface/ascent.cmi \
-    parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi lib/util.cmi \
-    contrib/interface_essai/xlate.cmi 
-contrib/interface_essai/xlate.cmx: contrib/interface/ascent.cmi \
-    parsing/ast.cmx parsing/coqast.cmx kernel/names.cmx lib/util.cmx \
-    contrib/interface_essai/xlate.cmi 
 contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \
     kernel/closure.cmi parsing/coqlib.cmi library/declare.cmi \
     kernel/environ.cmi tactics/equality.cmi proofs/evar_refiner.cmi \
-    kernel/evd.cmi library/global.cmi kernel/inductive.cmi proofs/logic.cmi \
-    kernel/names.cmi library/nametab.cmi contrib/omega/omega.cmo lib/pp.cmi \
+    library/global.cmi kernel/inductive.cmi proofs/logic.cmi kernel/names.cmi \
+    library/nametab.cmi contrib/omega/omega.cmo lib/pp.cmi \
     parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    pretyping/retyping.cmi kernel/sign.cmi proofs/tacmach.cmi \
-    tactics/tactics.cmi kernel/term.cmi lib/util.cmi 
+    kernel/sign.cmi proofs/tacmach.cmi tactics/tactics.cmi kernel/term.cmi \
+    lib/util.cmi 
 contrib/omega/coq_omega.cmx: parsing/ast.cmx proofs/clenv.cmx \
     kernel/closure.cmx parsing/coqlib.cmx library/declare.cmx \
     kernel/environ.cmx tactics/equality.cmx proofs/evar_refiner.cmx \
-    kernel/evd.cmx library/global.cmx kernel/inductive.cmx proofs/logic.cmx \
-    kernel/names.cmx library/nametab.cmx contrib/omega/omega.cmx lib/pp.cmx \
+    library/global.cmx kernel/inductive.cmx proofs/logic.cmx kernel/names.cmx \
+    library/nametab.cmx contrib/omega/omega.cmx lib/pp.cmx \
     parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \
-    pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx \
-    tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
+    kernel/sign.cmx proofs/tacmach.cmx tactics/tactics.cmx kernel/term.cmx \
+    lib/util.cmx 
 contrib/omega/omega.cmo: lib/util.cmi 
 contrib/omega/omega.cmx: lib/util.cmx 
 contrib/ring/quote.cmo: library/declare.cmi library/global.cmi \
@@ -2305,6 +1929,24 @@ contrib/ring/ring.cmx: parsing/astterm.cmx kernel/closure.cmx \
     proofs/tacmach.cmx pretyping/tacred.cmx tactics/tactics.cmx \
     kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx 
+contrib/romega/const_omega.cmo: library/declare.cmi library/global.cmi \
+    kernel/names.cmi kernel/reduction.cmi kernel/term.cmi lib/util.cmi 
+contrib/romega/const_omega.cmx: library/declare.cmx library/global.cmx \
+    kernel/names.cmx kernel/reduction.cmx kernel/term.cmx lib/util.cmx 
+contrib/romega/refl_omega.cmo: parsing/ast.cmi tactics/auto.cmi \
+    proofs/clenv.cmi contrib/romega/const_omega.cmo \
+    contrib/omega/coq_omega.cmo kernel/environ.cmi kernel/inductive.cmi \
+    proofs/logic.cmi kernel/names.cmi contrib/omega/omega.cmo lib/pp.cmi \
+    parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi lib/util.cmi 
+contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
+    proofs/clenv.cmx contrib/romega/const_omega.cmx \
+    contrib/omega/coq_omega.cmx kernel/environ.cmx kernel/inductive.cmx \
+    proofs/logic.cmx kernel/names.cmx contrib/omega/omega.cmx lib/pp.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 \
diff --git a/Makefile b/Makefile
index 79fbb96f3..daa2950fa 100644
--- a/Makefile
+++ b/Makefile
@@ -39,7 +39,8 @@ noargument:
 
 LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
               -I proofs -I tactics -I pretyping -I parsing -I toplevel  \
-              -I contrib/omega -I contrib/ring -I contrib/xml \
+              -I contrib/omega -I contrib/romega \
+	      -I contrib/ring -I contrib/xml \
 	      -I contrib/extraction -I contrib/correctness \
               -I contrib/interface -I contrib/fourier
 
@@ -183,6 +184,8 @@ ML4FILES += contrib/correctness/psyntax.ml4 contrib/field/field.ml4
 
 OMEGACMO=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo
 
+ROMEGACMO=contrib/romega/const_omega.cmo contrib/romega/refl_omega.cmo 
+
 RINGCMO=contrib/ring/quote.cmo contrib/ring/ring.cmo 
 
 FIELDCMO=contrib/field/field.cmo 
@@ -207,7 +210,8 @@ CORRECTNESSCMO=contrib/correctness/pmisc.cmo				\
 	contrib/correctness/pwp.cmo contrib/correctness/pmlize.cmo	\
 	contrib/correctness/ptactic.cmo	contrib/correctness/psyntax.cmo
 
-CONTRIB=$(OMEGACMO) $(RINGCMO) $(FIELDCMO) $(XMLCMO) $(FOURIERCMO) \
+CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) $(XMLCMO) \
+	$(FOURIERCMO) \
 	$(EXTRACTIONCMO) $(CORRECTNESSCMO)
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
@@ -478,6 +482,8 @@ OMEGAVO = contrib/omega/Omega.vo       contrib/omega/Zlogarithm.vo \
           contrib/omega/OmegaSyntax.vo contrib/omega/Zpower.vo \
           contrib/omega/Zcomplements.vo
 
+ROMEGAVO = contrib/romega/ReflOmegaCore.vo contrib/romega/ROmega.vo 
+
 RINGVO = contrib/ring/ArithRing.vo      contrib/ring/Ring_normalize.vo \
          contrib/ring/Ring_theory.vo    contrib/ring/Ring.vo \
          contrib/ring/ZArithRing.vo     contrib/ring/Ring_abstract.vo \
@@ -499,13 +505,14 @@ contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE)
 contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/initial.coq
 	$(COQC) -boot -byte  $(COQINCLUDES) $<
 
-CONTRIBVO = $(OMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) $(CORRECTNESSVO)\
+CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
+	    $(CORRECTNESSVO)\
             $(INTERFACEV0) $(FOURIERVO)
 
 $(CONTRIBVO): states/initial.coq
 
 contrib: $(CONTRIBVO) $(CONTRIBCMO)
-omega: $(OMEGAVO) $(OMEGACMO)
+omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
 ring: $(RINGVO) $(RINGCMO)
 # xml_ instead of xml to avoid conflict with "make xml"
 xml_: $(XMLVO) $(XMLCMO)
@@ -677,7 +684,7 @@ clean::
 
 tags:
 	find . -name "*.ml*" | sort -r | xargs \
-	etags "--regex='/let[ \t]+\([^ \t]+\)/\1/'" \
+	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
diff --git a/contrib/romega/README b/contrib/romega/README
new file mode 100644
index 000000000..c82087c7d
--- /dev/null
+++ b/contrib/romega/README
@@ -0,0 +1,19 @@
+This work was done for the RNRT Project Calife. 
+As such it is distributed under the LGPL licence.
+
+Change the COQTOP variable in the Makefile and type make. 
+The caml compiler should be in your path.
+
+WARNING : there is a bug in the 7.0 production release that prevents
+the compilation of the core ReflOmegaCore.v module. This development
+will only work with the beta release and (hopefully) subsequent version
+of Coq.
+
+A patch (patch-v7) contributed by D. Delahaye is included to correct the bug in
+regular 7.0 versions. It must be applied in the 'parsing' directory.
+Using it with a 7.0beta requires a few changes in const_omega.ml due to
+some changes in the paths of modules.
+
+Report bugs to :
+  pierre.cregut@francetelecom.com
+
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
new file mode 100644
index 000000000..0a140faf5
--- /dev/null
+++ b/contrib/romega/ROmega.v
@@ -0,0 +1,19 @@
+(*************************************************************************
+
+   PROJET RNRT Calife - 2001
+   Author: Pierre Crégut - France Télécom R&D
+   Licence : LGPL version 2.1
+
+ *************************************************************************)
+
+Require Omega.
+Require ReflOmegaCore.
+
+Declare ML Module "const_omega".
+Declare ML Module "refl_omega".
+
+Grammar tactic simple_tactic : ast :=
+  romega [ "ROmega" ] -> [(ReflOmega)].
+
+Syntax tactic level 0:
+  romega [ << (ReflOmega) >> ] -> ["ROmega"].        
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
new file mode 100644
index 000000000..9a4b299b4
--- /dev/null
+++ b/contrib/romega/ReflOmegaCore.v
@@ -0,0 +1,1885 @@
+(*************************************************************************
+
+   PROJET RNRT Calife - 2001
+   Author: Pierre Crégut - France Télécom R&D
+   Licence : LGPL version 2.1
+
+ *************************************************************************)
+
+Require Arith.
+Require PolyList.
+Require Bool.
+Require ZArith.
+
+(* \subsection{Définition des types} *)
+
+(* \subsubsection{Définition des termes dans Z réifiés}
+   Les termes comprennent les entiers relatifs [Tint] et les 
+   variables [Tvar] ainsi que les opérations de base sur Z (addition,
+   multiplication, opposé et soustraction). Les deux denières sont
+   rapidement traduites dans les deux premières durant la normalisation
+   des termes. *)
+
+Inductive term : Set :=
+   Tint : Z -> term
+ | Tplus : term -> term -> term
+ | Tmult : term -> term -> term
+ | Tminus : term -> term -> term
+ | Topp : term -> term
+ | Tvar : nat -> term
+.
+
+(* \subsubsection{Définition des buts réifiés} *)
+(* Définition très restreinte des prédicats manipulés (à enrichir). 
+   La prise en compte des négations et des diséquations demande la
+   prise en compte de la résolution en parallèle de plusieurs buts.
+   Ceci n'est possible qu'en modifiant de manière drastique la définition
+   de normalize qui doit pouvoir générer des listes de buts. Il faut
+   donc aussi modifier la normalisation qui peut elle aussi amener la
+   génération d'une liste de but et donc l'application d'une liste de
+   tactiques de résolution ([execute_omega])  *)
+Inductive proposition : Set :=
+  EqTerm : term -> term -> proposition
+| LeqTerm : term -> term -> proposition
+| TrueTerm : proposition
+| FalseTerm : proposition
+| Tnot : proposition -> proposition
+| GeqTerm : term -> term -> proposition
+| GtTerm : term -> term -> proposition
+| LtTerm : term -> term -> proposition
+| NeqTerm: term -> term -> proposition.
+
+(* Définition des hypothèses *)
+Syntactic Definition hyps := (list proposition).      
+
+Definition absurd := (cons FalseTerm (nil proposition)).
+
+(* \subsubsection{Traces de fusion d'équations} *)
+
+Inductive t_fusion : Set :=
+    F_equal : t_fusion | F_cancel : t_fusion
+  | F_left : t_fusion  | F_right : t_fusion.
+
+(* \subsection{Egalité décidable efficace} *)
+(* Pour chaque type de donnée réifié, on calcule un test d'égalité efficace.
+   Ce n'est pas le cas de celui rendu par [Decide Equality].
+   
+   Puis on prouve deux théorèmes permettant d'éliminer de telles égalités :
+   \begin{verbatim}
+   (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2.
+   (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2.
+   \end{verbatim} *)
+
+(* Ces deux tactiques permettent de résoudre pas mal de cas. L'une pour
+   les théorèmes positifs, l'autre pour les théorèmes négatifs *)
+
+Tactic Definition absurd_case := Simpl; Intros; Discriminate.
+Tactic Definition trivial_case := Unfold not; Intros; Discriminate.
+
+(* \subsubsection{Entiers naturels} *)
+
+Fixpoint eq_nat [t1,t2: nat] : bool := 
+  Cases t1 of
+    O => Cases t2 of O => true | _ => false end
+  | (S n1)=> Cases t2 of O => false | (S n2)  => (eq_nat n1 n2) end
+  end.
+
+Theorem eq_nat_true : (t1,t2: nat) (eq_nat t1 t2) = true -> t1 = t2.
+
+Induction t1; [
+  Intro t2; Case t2; [ Trivial | absurd_case ]
+| Intros n H t2; Case t2; 
+    [ absurd_case |  Simpl; Intros; Rewrite (H n0); [ Trivial | Assumption]]].
+
+Save.
+  
+Theorem eq_nat_false : (t1,t2: nat) (eq_nat t1 t2) = false -> ~t1 = t2.
+
+Induction t1; [
+  Intro t2; Case t2;
+   [ Simpl;Intros; Discriminate | trivial_case ]
+| Intros n H t2; Case t2; Simpl; Unfold not; Intros; [
+    Discriminate
+  | Elim (H n0 H0); Simplify_eq H1; Trivial]].
+
+Save.
+                                   
+
+(* \subsubsection{Entiers positifs} *)
+
+Fixpoint eq_pos [p1,p2 : positive] : bool := 
+  Cases p1 of
+    (xI n1) => Cases p2 of (xI n2) => (eq_pos n1 n2) | _ => false end
+  | (xO n1) =>  Cases p2 of (xO n2) => (eq_pos n1 n2) | _ => false end
+  | xH =>  Cases p2 of xH => true | _ => false end
+  end.
+
+Theorem eq_pos_true : (t1,t2: positive) (eq_pos t1 t2) = true -> t1 = t2.
+
+Induction t1; [
+  Intros p H t2; Case t2; [
+    Simpl; Intros; Rewrite (H p0 H0); Trivial | absurd_case | absurd_case ]
+| Intros p H t2; Case t2; [
+    absurd_case | Simpl; Intros; Rewrite (H p0 H0); Trivial | absurd_case ]
+| Intro t2; Case t2; [ absurd_case | absurd_case | Auto ]].
+
+Save.
+  
+Theorem eq_pos_false : (t1,t2: positive) (eq_pos t1 t2) = false -> ~t1 = t2.
+
+Induction t1; [
+  Intros p H t2; Case t2; [
+    Simpl; Unfold not; Intros; Elim (H p0 H0); Simplify_eq H1; Auto
+  | trivial_case | trivial_case ]
+| Intros p H t2; Case t2; [
+    trivial_case 
+  | Simpl; Unfold not; Intros; Elim (H p0 H0); Simplify_eq H1; Auto
+  | trivial_case ]
+| Intros t2; Case t2; [ trivial_case | trivial_case  | absurd_case ]].
+Save.
+
+(* \subsubsection{Entiers relatifs} *)
+
+Definition eq_Z [z1,z2: Z] : bool :=
+  Cases z1 of
+     ZERO     => Cases z2 of ZERO => true | _ => false end
+   | (POS p1) => Cases z2 of (POS p2) => (eq_pos p1 p2) | _ => false end
+   | (NEG p1) => Cases z2 of (NEG p2) => (eq_pos p1 p2) | _ => false end
+  end.
+
+Theorem eq_Z_true : (t1,t2: Z) (eq_Z t1 t2) = true -> t1 = t2.
+
+Induction t1; [
+  Intros t2; Case t2; [ Auto | absurd_case | absurd_case ]
+| Intros p t2; Case t2; [
+    absurd_case | Simpl; Intros; Rewrite (eq_pos_true p p0 H); Trivial 
+  | absurd_case ]
+| Intros p t2; Case t2; [
+    absurd_case | absurd_case
+  | Simpl; Intros; Rewrite (eq_pos_true p p0 H); Trivial ]].
+
+Save.
+
+Theorem eq_Z_false : (t1,t2: Z) (eq_Z t1 t2) = false -> ~(t1 = t2).
+
+Induction t1; [
+  Intros t2; Case t2; [ absurd_case | trivial_case | trivial_case ]
+| Intros p t2; Case t2; [
+    absurd_case
+  | Simpl; Unfold not; Intros; Elim (eq_pos_false p p0 H); Simplify_eq H0; Auto
+  | trivial_case ]
+| Intros p t2; Case t2; [
+    absurd_case | trivial_case 
+  | Simpl; Unfold not; Intros; Elim (eq_pos_false p p0 H); 
+    Simplify_eq H0; Auto]].
+Save.
+
+(* \subsubsection{Termes réifiés} *)
+
+Fixpoint eq_term [t1,t2: term] : bool := 
+   Cases t1 of
+      (Tint st1) =>
+         Cases t2 of (Tint st2) => (eq_Z st1 st2) | _ => false end
+    | (Tplus st11 st12) =>
+         Cases t2 of
+            (Tplus st21 st22) => 
+               (andb (eq_term st11 st21) (eq_term st12 st22))
+         | _ => false 
+         end
+    | (Tmult st11 st12) =>
+         Cases t2 of
+            (Tmult st21 st22) => 
+               (andb (eq_term st11 st21) (eq_term st12 st22))
+         | _ => false 
+         end
+    | (Tminus st11 st12) =>
+         Cases t2 of
+            (Tminus st21 st22) => 
+               (andb (eq_term st11 st21) (eq_term st12 st22))
+         | _ => false 
+         end
+    | (Topp st1) =>
+         Cases t2 of (Topp st2) => (eq_term st1 st2) | _ => false end
+    | (Tvar st1) =>
+         Cases t2 of (Tvar st2) => (eq_nat st1 st2) | _ => false end
+   end.  
+
+Theorem eq_term_true : (t1,t2: term) (eq_term t1 t2) = true -> t1 = t2.
+
+
+Induction t1; Intros until t2; Case t2; Try absurd_case; Simpl; [
+  Intros; Elim eq_Z_true with 1 := H; Trivial
+| Intros t21 t22 H3; Elim andb_prop with 1:= H3; Intros H4 H5; 
+  Elim H with 1 := H4; Elim H0 with 1 := H5; Trivial
+| Intros t21 t22 H3; Elim andb_prop with 1:= H3; Intros H4 H5;
+  Elim H with 1 := H4; Elim H0 with 1 := H5; Trivial
+| Intros t21 t22 H3; Elim andb_prop with 1:= H3; Intros H4 H5; 
+  Elim H with 1 := H4; Elim H0 with 1 := H5; Trivial
+| Intros t21 H3; Elim H with 1 := H3; Trivial
+| Intros; Elim eq_nat_true with 1 := H; Trivial ].
+
+Save.
+
+Theorem eq_term_false : (t1,t2: term) (eq_term t1 t2) = false -> ~(t1 = t2).
+
+Induction t1; [
+  Intros z t2; Case t2; Try trivial_case; Simpl; Unfold not; Intros;
+  Elim eq_Z_false with 1:=H; Simplify_eq H0; Auto
+| Intros t11 H1 t12 H2 t2; Case t2; Try trivial_case; Simpl; Intros t21 t22 H3;
+  Unfold not; Intro H4; Elim andb_false_elim with 1:= H3; Intros H5; 
+  [ Elim H1 with 1 := H5; Simplify_eq H4; Auto |
+    Elim H2 with 1 := H5; Simplify_eq H4; Auto ]
+| Intros t11 H1 t12 H2 t2; Case t2; Try trivial_case; Simpl; Intros t21 t22 H3;
+  Unfold not; Intro H4; Elim andb_false_elim with 1:= H3; Intros H5; 
+  [ Elim H1 with 1 := H5; Simplify_eq H4; Auto |
+    Elim H2 with 1 := H5; Simplify_eq H4; Auto ]
+| Intros t11 H1 t12 H2 t2; Case t2; Try trivial_case; Simpl; Intros t21 t22 H3;
+  Unfold not; Intro H4; Elim andb_false_elim with 1:= H3; Intros H5; 
+  [ Elim H1 with 1 := H5; Simplify_eq H4; Auto |
+    Elim H2 with 1 := H5; Simplify_eq H4; Auto ]
+| Intros t11 H1 t2; Case t2; Try trivial_case; Simpl; Intros t21 H3;
+  Unfold not; Intro H4; Elim H1 with 1 := H3; Simplify_eq H4; Auto 
+| Intros n t2; Case t2; Try trivial_case; Simpl; Unfold not; Intros;
+  Elim eq_nat_false with 1:=H; Simplify_eq H0; Auto ].
+
+Save.
+
+(* \subsubsection{Tactiques pour éliminer ces tests} 
+
+   Si on se contente de faire un [Case (eq_typ t1 t2)] on perd 
+   totalement dans chaque branche le fait que [t1=t2] ou [~t1=t2].
+
+   Initialement, les développements avaient été réalisés avec les
+   tests rendus par [Decide Equality], c'est à dire un test rendant
+   des termes du type [{t1=t2}+{~t1=t2}]. Faire une élimination sur un 
+   tel test préserve bien l'information voulue mais calculatoirement de
+   telles fonctions sont trop lentes. *)
+
+(* Le théorème suivant permet de garder dans les hypothèses la valeur
+   du booléen lors de l'élimination. *)
+
+Theorem bool_ind2 : 
+   (P:(bool->Prop)) (b:bool)
+     (b = true -> (P true))->
+     (b = false -> (P false)) -> (P b).
+
+Induction b; Auto.
+Save.
+
+(* Les tactiques définies si après se comportent exactement comme si on
+   avait utilisé le test précédent et fait une elimination dessus. *)
+
+Tactic Definition Elim_eq_term t1 t2 :=
+  Pattern (eq_term t1 t2); Apply bool_ind2; Intro Aux; [
+    Generalize (eq_term_true t1 t2 Aux); Clear Aux
+  | Generalize (eq_term_false t1 t2 Aux); Clear Aux ].
+
+Tactic Definition Elim_eq_Z t1 t2 :=
+  Pattern (eq_Z t1 t2); Apply bool_ind2; Intro Aux; [
+    Generalize (eq_Z_true t1 t2 Aux); Clear Aux
+  | Generalize (eq_Z_false t1 t2 Aux); Clear Aux ].
+
+Tactic Definition Elim_eq_pos t1 t2 :=
+  Pattern (eq_pos t1 t2); Apply bool_ind2; Intro Aux; [
+    Generalize (eq_pos_true t1 t2 Aux); Clear Aux
+  | Generalize (eq_pos_false t1 t2 Aux); Clear Aux ].
+
+(* \subsubsection{Comparaison sur Z} *)
+
+(* Sujet très lié au précédent : on introduit la tactique d'élimination
+   avec son théorème *)
+
+Theorem relation_ind2 : 
+   (P:(relation->Prop)) (b:relation)
+     (b = EGAL -> (P EGAL))->
+     (b = INFERIEUR -> (P INFERIEUR))->
+     (b = SUPERIEUR -> (P SUPERIEUR)) -> (P b).
+
+Induction b; Auto.
+Save.
+
+Tactic Definition Elim_Zcompare t1 t2 :=
+  Pattern (Zcompare t1 t2); Apply relation_ind2.
+
+(* \subsection{Interprétations}
+   \subsubsection{Interprétation des termes dans Z} *)
+
+Fixpoint interp_term [env:(list Z); t:term] : Z :=
+  Cases t of
+    (Tint x) => x
+  | (Tplus t1 t2) => (Zplus (interp_term env t1) (interp_term env t2))
+  | (Tmult t1 t2) => (Zmult (interp_term env t1) (interp_term env t2))
+  | (Tminus t1 t2) => (Zminus (interp_term env t1) (interp_term env t2))
+  | (Topp t) => (Zopp (interp_term env t))
+  | (Tvar n) => (nth n env ZERO)
+  end.
+
+(* \subsubsection{Interprétation des prédicats} *) 
+Fixpoint interp_proposition [env: (list Z); p:proposition] : Prop := 
+  Cases p of
+    (EqTerm t1 t2) => ((interp_term env t1) = (interp_term env t2))
+  | (LeqTerm t1 t2) => `(interp_term env t1) <= (interp_term env t2)`
+  | TrueTerm => True
+  | FalseTerm => False
+  | (Tnot p') => ~(interp_proposition env p')
+  | (GeqTerm t1 t2) => `(interp_term env t1) >= (interp_term env t2)`
+  | (GtTerm t1 t2) => `(interp_term env t1) > (interp_term env t2)`
+  | (LtTerm t1 t2) => `(interp_term env t1) < (interp_term env t2)`
+  | (NeqTerm t1 t2) => `(Zne (interp_term env t1) (interp_term env t2))`
+  end.
+
+(* \subsubsection{Inteprétation des listes d'hypothèses}
+   \paragraph{Sous forme de conjonction}
+   Interprétation sous forme d'une conjonction d'hypothèses plus faciles
+   à manipuler individuellement *)
+
+Fixpoint interp_hyps [env : (list Z); l: hyps] : Prop :=
+  Cases l of 
+     nil => True
+   | (cons p' l') => (interp_proposition env p') /\ (interp_hyps env l')
+  end.
+
+(* \paragraph{ous forme de but}
+   C'est cette interpétation que l'on utilise sur le but (car on utilise
+   [Generalize] et qu'une conjonction est forcément lourde (répétition des
+   types dans les conjonctions intermédiaires) *)
+
+Fixpoint interp_goal [env : (list Z); l: hyps] : Prop :=
+  Cases l of 
+     nil => False
+   | (cons p' l') => (interp_proposition env p') -> (interp_goal env l')
+  end.
+
+(* Les théorèmes qui suivent assurent la correspondance entre les deux
+   interprétations. *)
+
+Theorem goal_to_hyps : 
+  (env : (list Z); l: hyps) 
+     ((interp_hyps env l) -> False) -> (interp_goal env l).
+
+Induction l; [
+  Simpl; Auto
+| Simpl; Intros a l1 H1 H2 H3; Apply H1; Intro H4; Apply H2; Auto ].
+Save.
+
+Theorem hyps_to_goal : 
+  (env : (list Z); l: hyps) 
+     (interp_goal env l) -> ((interp_hyps env l) -> False).
+
+Induction l; Simpl; [
+  Auto
+| Intros; Apply H; Elim H1; Auto ].
+Save.
+      
+(* \subsection{Manipulations sur les hypothèses} *)
+
+(* \subsubsection{Définitions de base de stabilité pour la réflexion} *)
+(* Une opération laisse un terme stable si l'égalité est préservée *)
+Definition term_stable [f: term -> term] :=
+ (e: (list Z); t:term) (interp_term e t) = (interp_term e (f t)).
+
+(* Une opération est valide sur une hypothèse, si l'hypothèse implique le
+   résultat de l'opération. \emph{Attention : cela ne concerne que des 
+   opérations sur les hypothèses et non sur les buts (contravariance)}.
+   On définit la validité pour une opération prenant une ou deux propositions
+   en argument (cela suffit pour omega). *)
+
+Definition valid1 [f: proposition -> proposition] :=
+  (e: (list Z)) (p1: proposition) 
+    (interp_proposition e p1) -> (interp_proposition e (f p1)).
+
+Definition valid2 [f: proposition -> proposition -> proposition] :=
+  (e: (list Z)) (p1,p2: proposition) 
+    (interp_proposition e p1) -> (interp_proposition e p2) ->
+      (interp_proposition e (f p1 p2)).
+
+(* Dans cette notion de validité, la fonction prend directement une 
+   liste de propositions et rend une nouvelle liste de proposition. 
+   On reste contravariant *)
+
+Definition valid_hyps [f: hyps -> hyps] :=
+  (e : (list Z)) (lp: hyps) (interp_hyps e lp) -> (interp_hyps e (f lp)).
+
+(* Enfin ce théorème élimine la contravariance et nous ramène à une 
+   opération sur les buts *)
+
+Theorem valid_goal :
+  (env : (list Z); l: hyps; a : hyps -> hyps) 
+    (valid_hyps a) -> (interp_goal env (a l)) -> (interp_goal env l).
+
+Intros; Apply goal_to_hyps; Intro H1; Apply (hyps_to_goal env (a l) H0);
+Apply H; Assumption.
+Save.
+
+(* \subsubsection{Généralisation a des listes de buts (disjonctions)} *)
+
+Syntactic Definition lhyps := (list hyps).
+
+Fixpoint interp_list_hyps [env: (list Z); l : lhyps] : Prop :=
+   Cases l of
+      nil => False
+    | (cons h l') => (interp_hyps env h) \/ (interp_list_hyps env l')
+   end.
+
+Fixpoint interp_list_goal [env: (list Z);l : lhyps] : Prop :=
+   Cases l of
+      nil => True
+    | (cons h l') => (interp_goal env h) /\ (interp_list_goal env l')
+   end.
+
+Theorem list_goal_to_hyps : 
+  (env: (list Z); l: lhyps)
+    ((interp_list_hyps env l) -> False) -> (interp_list_goal env l).
+
+Induction l; Simpl; [
+  Auto
+| Intros h1 l1 H H1; Split; [
+    Apply goal_to_hyps; Intro H2; Apply H1; Auto
+  | Apply H; Intro H2; Apply H1; Auto ]].
+Save.
+
+Theorem list_hyps_to_goal : 
+  (env: (list Z); l: lhyps)
+    (interp_list_goal env l) -> ((interp_list_hyps env l) -> False).
+
+Induction l; Simpl; [
+  Auto
+|  Intros h1 l1 H (H1,H2) H3; Elim H3; Intro H4; [
+     Apply hyps_to_goal with 1 := H1; Assumption
+   | Auto ]].
+Save.
+
+Definition valid_list_hyps [f: hyps -> lhyps] :=
+  (e : (list Z)) (lp: hyps) (interp_hyps e lp) -> (interp_list_hyps e (f lp)).
+
+Definition valid_list_goal [f: hyps -> lhyps] :=
+  (e : (list Z)) (lp: hyps) 
+     (interp_list_goal e (f lp)) -> (interp_goal e lp) .
+
+Theorem goal_valid : 
+  (f: hyps -> lhyps) (valid_list_hyps f) -> (valid_list_goal f).
+
+Unfold valid_list_goal; Intros f H e lp H1; Apply goal_to_hyps;
+Intro H2; Apply list_hyps_to_goal with 1:=H1; Apply (H e lp); Assumption.
+Save.
+ 
+Theorem append_valid :
+  (e: (list Z)) (l1,l2:lhyps)
+     (interp_list_hyps e l1) \/ (interp_list_hyps e l2) ->
+     (interp_list_hyps e (app l1 l2)).
+
+Intros e; Induction l1; [
+  Simpl; Intros l2 [H | H]; [ Contradiction | Trivial ]
+| Simpl; Intros h1 t1 HR l2 [[H | H] | H] ;[
+    Auto
+  | Right; Apply (HR l2); Left; Trivial
+  | Right; Apply (HR l2); Right; Trivial ]].
+
+Save.
+
+(* \subsubsection{Opérateurs valides sur les hypothèses} *)
+
+(* Extraire une hypothèse de la liste *)
+Definition nth_hyps [n:nat; l: hyps] := (nth n l TrueTerm).
+
+Theorem nth_valid :
+  (e: (list Z); i:nat; l: hyps) 
+     (interp_hyps e l) -> (interp_proposition e (nth_hyps i l)).
+
+Unfold nth_hyps; Induction i; [
+  Induction l; Simpl; [ Auto | Intros; Elim H0; Auto ]
+| Intros n H; Induction l;
+    [ Simpl; Trivial | Intros; Simpl; Apply H; Elim H1; Auto ]].
+Save.
+
+(* Appliquer une opération (valide) sur deux hypothèses extraites de 
+   la liste et ajouter le résultat à la liste. *)
+Definition apply_oper_2 
+  [i,j : nat; f : proposition -> proposition -> proposition ] :=
+  [l: hyps] (cons (f (nth_hyps i l)  (nth_hyps j l)) l).
+
+Theorem apply_oper_2_valid :
+  (i,j : nat; f : proposition -> proposition -> proposition )
+    (valid2 f) -> (valid_hyps (apply_oper_2 i j f)).
+
+Intros i j f Hf; Unfold apply_oper_2 valid_hyps; Simpl; Intros lp Hlp; Split;
+  [ Apply Hf; Apply nth_valid; Assumption | Assumption].
+Save.
+
+(* Modifier une hypothèse par application d'une opération valide *)
+
+Fixpoint apply_oper_1 [i:nat] : (proposition -> proposition) -> hyps -> hyps :=
+  [f : (proposition -> proposition); l : hyps] 
+    Cases l of 
+       nil => (nil proposition)
+    | (cons p l') =>
+	 Cases i of
+           O => (cons (f p) l')
+         | (S j) => (cons p (apply_oper_1 j f l'))
+         end
+    end.
+
+Theorem apply_oper_1_valid :
+  (i : nat; f : proposition -> proposition )
+    (valid1 f) -> (valid_hyps (apply_oper_1 i f)).
+
+Unfold valid_hyps; Intros i f Hf e; Elim i; [
+  Intro lp; Case lp; [
+    Simpl; Trivial
+  | Simpl; Intros p l' (H1, H2); Split; [ Apply Hf with 1:=H1 | Assumption ]]
+| Intros n Hrec lp; Case lp; [
+    Simpl; Auto
+  | Simpl; Intros p l' (H1, H2); 
+    Split; [ Assumption | Apply Hrec; Assumption ]]].
+
+Save.
+
+(* \subsubsection{Manipulations de termes} *)
+(* Les fonctions suivantes permettent d'appliquer une fonction de
+   réécriture sur un sous terme du terme principal. Avec la composition,
+   cela permet de construire des réécritures complexes proches des 
+   tactiques de conversion *)
+
+Definition apply_left [f: term -> term; t : term]:= 
+  Cases t of
+    (Tplus x y) => (Tplus (f x) y)
+  | (Tmult x y) => (Tmult (f x) y)
+  | (Topp x) => (Topp (f x))
+  | x => x
+  end.
+
+Definition apply_right [f: term -> term; t : term]:= 
+  Cases t of
+    (Tplus x y) => (Tplus x (f y))
+  | (Tmult x y) => (Tmult x (f y))
+  | x => x
+  end.
+
+Definition apply_both [f,g: term -> term; t : term]:= 
+  Cases t of
+    (Tplus x y) => (Tplus (f x) (g y))
+  | (Tmult x y) => (Tmult (f x) (g y))
+  | x => x
+  end.
+
+(* Les théorèmes suivants montrent la stabilité (conditionnée) des 
+   fonctions. *)
+
+Theorem apply_left_stable :
+  (f: term -> term) (term_stable f) -> (term_stable (apply_left f)).
+
+Unfold term_stable; Intros f H e t; Case t; Auto; Simpl; 
+Intros;  Elim H; Trivial.
+Save.
+
+Theorem apply_right_stable :
+  (f: term -> term) (term_stable f) -> (term_stable (apply_right f)).
+
+Unfold term_stable; Intros f H e t; Case t; Auto; Simpl; 
+Intros t0 t1; Elim H; Trivial.
+Save.
+
+Theorem apply_both_stable :
+  (f,g: term -> term) (term_stable f) -> (term_stable g) -> 
+     (term_stable (apply_both f g)).
+
+Unfold term_stable; Intros f g H1 H2 e t; Case t; Auto; Simpl; 
+Intros t0 t1; Elim H1; Elim H2; Trivial.
+Save.
+
+Theorem compose_term_stable :
+  (f,g: term -> term) (term_stable f) -> (term_stable g) -> 
+    (term_stable [t: term](f (g t))).
+
+Unfold term_stable; Intros f g Hf Hg e t; Elim Hf; Apply Hg.
+Save.
+
+(* \subsection{Les règles de réécriture} *)
+(* Chacune des règles de réécriture est accompagnée par sa preuve de 
+   stabilité. Toutes ces preuves ont la même forme : il faut analyser 
+   suivant la forme du terme (élimination de chaque Case). On a besoin d'une
+   élimination uniquement dans les cas d'utilisation d'égalité décidable. 
+
+   Cette tactique itère la décomposition des Case. Elle est
+   constituée de deux fonctions s'appelant mutuellement :
+   \begin{itemize} 
+    \item une fonction d'enrobage qui lance la recherche sur le but,
+    \item une fonction récursive qui décompose ce but. Quand elle a trouvé un
+          Case, elle l'élimine. 
+   \end{itemize}  
+   Les motifs sur les cas sont très imparfaits et dans certains cas, il
+   semble que cela ne marche pas. On aimerait plutot un motif de la
+   forme [ Case (?1 :: T) of _ end ] permettant de s'assurer que l'on 
+   utilise le bon type.
+
+   Chaque élimination introduit correctement exactement le nombre d'hypothèses
+   nécessaires et conserve dans le cas d'une égalité la connaissance du
+   résultat du test en faisant la réécriture. Pour un test de comparaison,
+   on conserve simplement le résultat.
+
+   Cette fonction déborde très largement la résolution des réécritures
+   simples et fait une bonne partie des preuves des pas de Omega.
+*)
+
+(* \subsubsection{La tactique pour prouver la stabilité} *)
+Recursive Tactic Definition loop t := (
+  Match t With
+  (* Global *)
+    [(?1 = ?2)] -> (loop ?1) Orelse (loop ?2)
+  | [ ? -> ?1 ] ->  (loop ?1)
+  (* Interprétations *)
+  | [ (interp_hyps ? ?1) ] -> (loop ?1)
+  | [ (interp_list_hyps ? ?1) ] -> (loop ?1)
+  | [ (interp_proposition ? ?1) ] -> (loop ?1)
+  | [ (interp_term ? ?1) ] -> (loop ?1)
+  (* Propositions *)
+  | [(EqTerm ?1 ?2)] -> (loop ?1) Orelse (loop ?2)
+  | [(LeqTerm ?1 ?2)] -> (loop ?1) Orelse (loop ?2)
+  (* Termes *)
+  | [(Tplus ?1 ?2)] -> (loop ?1) Orelse (loop ?2)
+  | [(Tminus ?1 ?2)] -> (loop ?1) Orelse (loop ?2)
+  | [(Tmult ?1 ?2)] -> (loop ?1) Orelse (loop ?2)
+  | [(Topp ?1)] -> (loop ?1)
+  | [(Tint ?1)] -> (loop ?1)
+  (* Eliminations *)
+  | [(Case ?1 of ? ? ? ?   ? ? ? ?  ? end)] -> 
+       (Case ?1; [ Intro; Intro | Intro; Intro | Idtac | Idtac 
+                 | Intro | Intro; Intro | Intro; Intro | Intro; Intro
+                 | Intro; Intro ]);
+        Auto; (Simplify ())
+  | [(Case ?1 of ? ? ? ? ? ? end)] -> 
+       (Case ?1; [ Intro | Intro; Intro | Intro; Intro | Intro; Intro | 
+                   Intro | Intro ]); Auto; (Simplify ())
+  | [(Case (Zcompare ?1 ?2) of ? ? ? end)] -> 
+       (Elim_Zcompare ?1 ?2) ; Intro ; Auto; (Simplify ())
+  | [(Case ?1 of ? ? ? end)] -> 
+       (Case ?1; [ Idtac | Intro | Intro ]); Auto; (Simplify ())
+  | [(Case (eq_Z ?1 ?2) of ? ? end)] -> 
+       ((Elim_eq_Z ?1 ?2); Intro H; [Rewrite H; Clear H | Clear H]);
+       Simpl; Auto; (Simplify ())
+  | [(Case (eq_term ?1 ?2) of ? ? end)] -> 
+       ((Elim_eq_term ?1 ?2); Intro H; [Rewrite H; Clear H | Clear H]); 
+       Simpl; Auto; (Simplify ())
+  | [(Case (eq_pos ?1 ?2) of ? ? end)] -> 
+       ((Elim_eq_pos ?1 ?2); Intro H; [Rewrite H; Clear H | Clear H]);
+       Simpl; Auto; (Simplify ())
+  | _ -> Fail)
+And Simplify () := (
+  Match Context With [|- ?1 ] -> Try (loop ?1) | _ -> Idtac).
+
+(* L'utilisation de Match n'est qu'un hack pour contourner un bug de la 7.0 *)
+Tactic Definition ProveStable x th :=
+  (Match x With [?1] -> Unfold term_stable ?1; Intros; (Simplify ()); Simpl; Apply th).
+
+(* \subsubsection{Les règles elle mêmes} *)
+Definition Tplus_assoc_l [t: term] :=
+  Cases t of
+    (Tplus n (Tplus m p)) => (Tplus (Tplus n m) p)
+  | _ => t
+  end.
+
+Theorem  Tplus_assoc_l_stable : (term_stable  Tplus_assoc_l).
+
+(ProveStable Tplus_assoc_l Zplus_assoc_l).
+Save.
+
+Definition Tplus_assoc_r [t: term] :=
+  Cases t of
+    (Tplus (Tplus n m) p) => (Tplus n (Tplus m p))
+  | _ => t
+  end.
+
+Theorem  Tplus_assoc_r_stable : (term_stable  Tplus_assoc_r).
+
+(ProveStable Tplus_assoc_r Zplus_assoc_r).
+Save.
+
+Definition Tmult_assoc_r [t: term] :=
+  Cases t of
+    (Tmult (Tmult n m) p) => (Tmult n (Tmult m p))
+  | _ => t
+  end.
+
+Theorem  Tmult_assoc_r_stable : (term_stable  Tmult_assoc_r).
+
+(ProveStable Tmult_assoc_r Zmult_assoc_r).
+Save.
+
+Definition Tplus_permute [t: term] :=
+  Cases t of
+    (Tplus n (Tplus m p)) => (Tplus m (Tplus n p))
+  | _ => t
+  end.
+
+Theorem  Tplus_permute_stable : (term_stable  Tplus_permute).
+
+(ProveStable Tplus_permute Zplus_permute).
+Save.
+
+Definition Tplus_sym [t: term] :=
+  Cases t of
+    (Tplus x y) => (Tplus y x)
+  | _ => t
+  end.
+
+Theorem Tplus_sym_stable : (term_stable Tplus_sym).
+
+(ProveStable Tplus_sym Zplus_sym).
+Save.
+
+Definition Tmult_sym [t: term] :=
+  Cases t of
+    (Tmult x y) => (Tmult y x)
+  | _ => t
+  end.
+
+Theorem Tmult_sym_stable : (term_stable Tmult_sym).
+
+(ProveStable Tmult_sym Zmult_sym).
+Save.
+
+Definition T_OMEGA10 [t: term] :=
+  Cases t of
+    (Tplus (Tmult (Tplus (Tmult v (Tint c1)) l1) (Tint k1))
+           (Tmult (Tplus (Tmult v' (Tint c2)) l2) (Tint k2))) =>
+	Case (eq_term v v') of
+	    (Tplus (Tmult v (Tint (Zplus (Zmult c1 k1) (Zmult c2 k2)))) 
+                   (Tplus (Tmult l1 (Tint k1)) (Tmult l2 (Tint k2))))
+           t
+        end
+  | _ => t
+  end.
+
+Theorem  T_OMEGA10_stable : (term_stable  T_OMEGA10).
+
+(ProveStable T_OMEGA10 OMEGA10).
+Save.
+
+Definition T_OMEGA11 [t: term] :=
+  Cases t of
+    (Tplus (Tmult (Tplus (Tmult v1 (Tint c1)) l1) (Tint k1)) l2) =>
+	(Tplus (Tmult v1 (Tint (Zmult c1 k1))) (Tplus (Tmult l1 (Tint k1)) l2))
+  | _ => t
+  end.
+
+Theorem  T_OMEGA11_stable : (term_stable  T_OMEGA11).
+
+(ProveStable T_OMEGA11 OMEGA11).
+Save.
+
+Definition T_OMEGA12 [t: term] :=
+  Cases t of
+    (Tplus l1 (Tmult (Tplus (Tmult v2 (Tint c2)) l2) (Tint k2))) =>
+        (Tplus (Tmult v2 (Tint (Zmult c2 k2))) (Tplus l1 (Tmult l2 (Tint k2))))
+  | _ => t
+  end.
+
+Theorem  T_OMEGA12_stable : (term_stable  T_OMEGA12).
+
+(ProveStable T_OMEGA12 OMEGA12).
+Save. 
+
+Definition T_OMEGA13 [t: term] :=
+  Cases t of
+    (Tplus (Tplus (Tmult v (Tint (POS x))) l1) 
+	   (Tplus (Tmult v' (Tint (NEG x'))) l2)) =>
+	Case (eq_term v v') of
+	  Case (eq_pos x x') of
+	    (Tplus l1 l2)
+            t
+	  end
+	  t
+	end
+  | (Tplus (Tplus (Tmult v (Tint (NEG x))) l1) 
+	   (Tplus (Tmult v' (Tint (POS x'))) l2)) =>
+	Case (eq_term v v') of
+	  Case (eq_pos x x') of
+	    (Tplus l1 l2)
+             t
+	  end
+	  t
+	end
+
+  | _ => t
+  end.
+
+Theorem  T_OMEGA13_stable : (term_stable  T_OMEGA13).
+
+Unfold term_stable T_OMEGA13; Intros; (Simplify ()); Simpl; 
+  [ Apply OMEGA13 | Apply OMEGA14 ].
+Save.
+
+Definition T_OMEGA15 [t: term] :=
+  Cases t of
+    (Tplus (Tplus (Tmult v (Tint c1)) l1) 
+	   (Tmult (Tplus (Tmult v' (Tint c2)) l2) (Tint k2))) =>
+	Case (eq_term v v') of
+	  (Tplus (Tmult v (Tint (Zplus c1 (Zmult c2 k2))))
+	                  (Tplus l1 (Tmult l2 (Tint k2))))
+	  t
+	end
+  | _ => t
+  end.
+
+Theorem  T_OMEGA15_stable : (term_stable  T_OMEGA15).
+
+(ProveStable T_OMEGA15 OMEGA15).
+Save.
+
+Definition T_OMEGA16 [t: term] :=
+  Cases t of
+    (Tmult (Tplus (Tmult v (Tint c)) l) (Tint k)) =>
+       (Tplus (Tmult v (Tint (Zmult c k))) (Tmult l (Tint k)))
+  | _ => t
+  end.
+
+
+Theorem  T_OMEGA16_stable : (term_stable  T_OMEGA16).
+
+(ProveStable T_OMEGA16 OMEGA16).
+Save.
+
+Definition Tred_factor5 [t: term] := 
+   Cases t of
+      (Tplus (Tmult x (Tint ZERO)) y) => y
+   | _ => t
+   end.
+
+Theorem Tred_factor5_stable : (term_stable  Tred_factor5).
+
+
+(ProveStable Tred_factor5 Zred_factor5).
+Save.
+
+Definition Topp_plus [t: term] :=
+  Cases t of
+    (Topp (Tplus x y)) => (Tplus (Topp x) (Topp y))
+  | _ => t
+  end.
+
+Theorem Topp_plus_stable : (term_stable Topp_plus).
+
+(ProveStable Topp_plus Zopp_Zplus).
+Save.
+
+
+Definition Topp_opp [t: term] :=
+  Cases t of
+    (Topp (Topp x)) => x
+  | _ => t
+  end.
+
+Theorem Topp_opp_stable : (term_stable Topp_opp).
+
+(ProveStable Topp_opp Zopp_Zopp).
+Save.
+
+Definition Topp_mult_r [t: term] :=
+  Cases t of
+    (Topp (Tmult x (Tint k))) => (Tmult x (Tint (Zopp k)))
+  | _ => t
+  end.
+
+Theorem Topp_mult_r_stable : (term_stable Topp_mult_r).
+
+(ProveStable Topp_mult_r Zopp_Zmult_r).
+Save.
+
+Definition Topp_one [t: term] :=
+  Cases t of
+    (Topp x) => (Tmult x (Tint `-1`))
+  | _ => t
+  end.
+
+Theorem Topp_one_stable : (term_stable Topp_one).
+
+(ProveStable Topp_one Zopp_one).
+Save.
+
+Definition Tmult_plus_distr  [t: term] :=
+  Cases t of
+    (Tmult (Tplus n m) p) => (Tplus (Tmult n p) (Tmult m p))
+  | _ => t
+  end.
+
+Theorem Tmult_plus_distr_stable : (term_stable Tmult_plus_distr).
+
+(ProveStable Tmult_plus_distr Zmult_plus_distr).
+Save.
+
+Definition Tmult_opp_left [t: term] :=
+  Cases t of
+    (Tmult (Topp x) (Tint y)) => (Tmult x (Tint (Zopp y)))
+  | _ => t
+  end.
+
+Theorem Tmult_opp_left_stable : (term_stable Tmult_opp_left).
+
+(ProveStable Tmult_opp_left Zmult_Zopp_left).
+Save.
+
+Definition Tmult_assoc_reduced [t: term] :=
+  Cases t of
+    (Tmult (Tmult n (Tint m)) (Tint p)) => (Tmult n (Tint (Zmult m p)))
+  | _ => t
+  end.
+
+Theorem  Tmult_assoc_reduced_stable : (term_stable  Tmult_assoc_reduced).
+
+(ProveStable Tmult_assoc_reduced Zmult_assoc_r).
+Save.
+
+Definition Tred_factor0 [t: term] := (Tmult t (Tint `1`)).
+
+Theorem  Tred_factor0_stable : (term_stable  Tred_factor0).
+
+(ProveStable Tred_factor0 Zred_factor0).
+Save.
+
+Definition Tred_factor1 [t: term] :=
+  Cases t of
+    (Tplus x y) => 
+	Case (eq_term x y) of
+	  (Tmult x (Tint `2`))
+	  t
+        end
+  | _ => t
+  end.
+
+Theorem  Tred_factor1_stable : (term_stable  Tred_factor1).
+
+(ProveStable Tred_factor1 Zred_factor1).
+Save.
+
+Definition Tred_factor2 [t: term] :=
+  Cases t of
+    (Tplus x (Tmult y (Tint k))) => 
+	Case (eq_term x y) of
+	  (Tmult x (Tint (Zplus `1` k)))
+	  t
+        end
+  | _ => t
+  end.
+
+(* Attention : il faut rendre opaque [Zplus] pour éviter que la tactique
+   de simplification n'aille trop loin et défasse [Zplus 1 k] *)
+
+Opaque Zplus.
+
+Theorem  Tred_factor2_stable : (term_stable  Tred_factor2).
+(ProveStable Tred_factor2 Zred_factor2).
+Save.
+
+Definition Tred_factor3 [t: term] :=
+  Cases t of
+    (Tplus (Tmult x (Tint k)) y) => 
+	Case (eq_term x y) of
+	  (Tmult x (Tint `1+k`))
+	  t
+        end
+  | _ => t
+  end.
+
+Theorem  Tred_factor3_stable : (term_stable  Tred_factor3).
+
+(ProveStable Tred_factor3 Zred_factor3).
+Save.
+
+
+Definition Tred_factor4 [t: term] :=
+  Cases t of
+    (Tplus (Tmult x (Tint k1)) (Tmult y (Tint k2))) => 
+	Case (eq_term x y) of
+	  (Tmult x (Tint `k1+k2`))
+	  t
+        end
+  | _ => t
+  end.
+
+Theorem  Tred_factor4_stable : (term_stable  Tred_factor4).
+
+(ProveStable Tred_factor4 Zred_factor4).
+Save.
+
+Definition Tred_factor6 [t: term] := (Tplus t (Tint `0`)).
+
+Theorem  Tred_factor6_stable : (term_stable  Tred_factor6).
+
+(ProveStable Tred_factor6 Zred_factor6).
+Save.
+
+Transparent Zplus.
+
+Definition Tminus_def [t:term] :=
+  Cases t of
+    (Tminus x y) => (Tplus x (Topp y))
+  | _ => t
+  end.
+
+Theorem  Tminus_def_stable : (term_stable  Tminus_def).
+
+(* Le théorème ne sert à rien. Le but est prouvé avant. *)
+(ProveStable Tminus_def False).
+Save.
+
+(* \subsection{Fonctions de réécriture complexes} *)
+
+(* \subsubsection{Fonction de réduction} *)
+(* Cette fonction réduit un terme dont la forme normale est un entier. Il
+   suffit pour cela d'échanger le constructeur [Tint] avec les opérateurs
+   réifiés. La réduction est ``gratuite''.  *)
+
+Fixpoint reduce [t:term] : term :=
+  Cases t of
+     (Tplus x y) =>
+	 Cases (reduce x) of
+	   (Tint x') =>
+	      Cases (reduce y) of
+	        (Tint y') => (Tint (Zplus x' y'))
+              | y' => (Tplus (Tint x') y')
+              end
+         | x' => (Tplus x' (reduce y))
+	 end
+  | (Tmult x y) =>
+	 Cases (reduce x) of
+	   (Tint x') =>
+	      Cases (reduce y) of
+	        (Tint y') => (Tint (Zmult x' y'))
+              | y' => (Tmult (Tint x') y')
+              end
+         | x' => (Tmult x' (reduce y))
+	 end
+  | (Tminus x y) =>
+	 Cases (reduce x) of
+	   (Tint x') =>
+	      Cases (reduce y) of
+	        (Tint y') => (Tint (Zminus x' y'))
+              | y' => (Tminus (Tint x') y')
+              end
+         | x' => (Tminus x' (reduce y))
+	 end
+  | (Topp x) =>
+        Cases (reduce x) of
+	  (Tint x') => (Tint (Zopp x'))
+	| x' => (Topp x')
+	end
+  | _ => t
+  end.
+
+Theorem reduce_stable : (term_stable reduce).
+
+Unfold term_stable; Intros e t; Elim t; Auto; 
+Try (Intros t0 H0 t1 H1; Simpl; Rewrite H0; Rewrite H1; (
+ Case (reduce t0); [ 
+   Intro z0; Case (reduce t1); Intros; Auto
+ | Intros; Auto
+ | Intros; Auto
+ | Intros; Auto
+ | Intros; Auto
+ | Intros; Auto ]));
+Intros t0 H0; Simpl; Rewrite H0; Case (reduce t0); Intros; Auto.
+Save.
+
+(* \subsubsection{Fusions}
+    \paragraph{Fusion de deux équations} *)
+(* On donne une somme de deux équations qui sont supposées normalisées. 
+   Cette fonction prend une trace de fusion en argument et transforme
+   le terme en une équation normalisée. C'est une version très simplifiée
+   du moteur de réécriture [rewrite]. *)
+
+Fixpoint fusion [trace : (list t_fusion)] : term -> term := [t: term]
+  Cases trace of
+    nil => (reduce t)
+  | (cons step trace') =>
+	Cases step of
+        | F_equal => 
+	    (apply_right (fusion trace') (T_OMEGA10 t))
+        | F_cancel => 
+	    (fusion trace' (Tred_factor5 (T_OMEGA10 t)))
+        | F_left => 
+	    (apply_right (fusion trace') (T_OMEGA11 t))
+        | F_right =>
+	    (apply_right (fusion trace') (T_OMEGA12 t))
+	end
+  end.
+    
+Theorem fusion_stable : (t : (list t_fusion)) (term_stable (fusion t)).
+
+Induction t; Simpl; [
+  Exact reduce_stable
+| Intros step l H; Case step; [
+    Apply compose_term_stable; 
+      [ Apply apply_right_stable; Assumption | Exact T_OMEGA10_stable ]
+  | Unfold term_stable; Intros e t1; Rewrite T_OMEGA10_stable; 
+    Rewrite Tred_factor5_stable; Apply H
+  | Apply compose_term_stable; 
+      [ Apply apply_right_stable; Assumption | Exact T_OMEGA11_stable ]
+  | Apply compose_term_stable;
+      [ Apply apply_right_stable; Assumption | Exact T_OMEGA12_stable ]]].
+
+Save.
+
+(* \paragraph{Fusion de deux équations dont une sans coefficient} *)
+
+Definition fusion_right [trace : (list t_fusion)] : term -> term := [t: term]
+  Cases trace of
+    nil => (reduce t)  (* Il faut mettre un compute *)
+  | (cons step trace') =>
+	Cases step of
+        | F_equal => 
+	    (apply_right (fusion trace') (T_OMEGA15 t))
+        | F_cancel => 
+	    (fusion trace' (Tred_factor5 (T_OMEGA15 t)))
+        | F_left => 
+	    (apply_right (fusion trace') (Tplus_assoc_r t))
+        | F_right =>
+	    (apply_right (fusion trace') (T_OMEGA12 t))
+	end
+  end.
+
+(* \paragraph{Fusion avec anihilation} *)
+(* Normalement le résultat est une constante *)
+
+Fixpoint fusion_cancel [trace:nat] : term -> term := [t:term]
+  Cases trace of
+    O => (reduce t)
+  | (S trace') => (fusion_cancel trace' (T_OMEGA13 t))
+  end.
+
+Theorem fusion_cancel_stable : (t:nat) (term_stable (fusion_cancel t)).
+
+Unfold term_stable fusion_cancel; Intros trace e; Elim trace; [
+  Exact (reduce_stable e)
+| Intros n H t; Elim H; Exact (T_OMEGA13_stable e t) ].
+Save. 
+
+(* \subsubsection{Opérations afines sur une équation} *)
+(* \paragraph{Multiplication scalaire et somme d'une constante} *)
+
+Fixpoint scalar_norm_add [trace:nat] : term -> term := [t: term]
+  Cases trace of
+    O => (reduce t)
+  | (S trace') => (apply_right (scalar_norm_add trace') (T_OMEGA11 t))
+  end.
+
+Theorem scalar_norm_add_stable : (t:nat) (term_stable (scalar_norm_add t)).
+
+Unfold term_stable scalar_norm_add; Intros trace; Elim trace; [
+  Exact reduce_stable
+| Intros n H e t; Elim apply_right_stable; 
+    [ Exact (T_OMEGA11_stable e t) | Exact H ]].
+Save.
+   
+(* \paragraph{Multiplication scalaire} *)
+Fixpoint scalar_norm [trace:nat] : term -> term := [t: term]
+  Cases trace of
+    O => (reduce t)
+  | (S trace') => (apply_right (scalar_norm trace') (T_OMEGA16 t))
+  end.
+
+Theorem scalar_norm_stable : (t:nat) (term_stable (scalar_norm t)).
+
+Unfold term_stable scalar_norm; Intros trace; Elim trace; [
+  Exact reduce_stable
+| Intros n H e t; Elim apply_right_stable;
+    [ Exact (T_OMEGA16_stable e t) | Exact H ]].
+Save.
+
+(* \paragraph{Somme d'une constante} *)
+Fixpoint add_norm [trace:nat] : term -> term := [t: term]
+  Cases trace of
+    O => (reduce t)
+  | (S trace') => (apply_right (add_norm trace') (Tplus_assoc_r t))
+  end.
+
+Theorem add_norm_stable : (t:nat) (term_stable (add_norm t)).
+
+Unfold term_stable add_norm; Intros trace; Elim trace; [
+  Exact reduce_stable
+| Intros n H e t; Elim apply_right_stable;
+    [ Exact (Tplus_assoc_r_stable e t) | Exact H ]].
+Save.
+
+(* \subsection{La fonction de normalisation des termes (moteur de réécriture)} *)
+
+Inductive step : Set := 
+ | C_DO_BOTH : step -> step -> step
+ | C_LEFT : step -> step
+ | C_RIGHT : step -> step
+ | C_SEQ : step -> step -> step
+ | C_NOP : step
+ | C_OPP_PLUS : step
+ | C_OPP_OPP : step
+ | C_OPP_MULT_R : step
+ | C_OPP_ONE : step
+ | C_REDUCE : step
+ | C_MULT_PLUS_DISTR : step
+ | C_MULT_OPP_LEFT : step
+ | C_MULT_ASSOC_R : step
+ | C_PLUS_ASSOC_R : step
+ | C_PLUS_ASSOC_L : step
+ | C_PLUS_PERMUTE : step
+ | C_PLUS_SYM : step
+ | C_RED0 : step
+ | C_RED1 : step
+ | C_RED2 : step
+ | C_RED3 : step
+ | C_RED4 : step
+ | C_RED5 : step
+ | C_RED6 : step
+ | C_MULT_ASSOC_REDUCED : step
+ | C_MINUS :step
+ | C_MULT_SYM : step
+.
+
+Fixpoint rewrite [s: step] : term -> term :=
+  Cases s of 
+   | (C_DO_BOTH s1 s2) => (apply_both (rewrite s1) (rewrite s2))
+   | (C_LEFT s) => (apply_left (rewrite s))
+   | (C_RIGHT s) => (apply_right (rewrite s))
+   | (C_SEQ s1 s2) => [t: term] (rewrite s2 (rewrite s1 t))
+   | C_NOP => [t:term] t
+   | C_OPP_PLUS => Topp_plus
+   | C_OPP_OPP => Topp_opp
+   | C_OPP_MULT_R => Topp_mult_r
+   | C_OPP_ONE => Topp_one
+   | C_REDUCE => reduce
+   | C_MULT_PLUS_DISTR => Tmult_plus_distr
+   | C_MULT_OPP_LEFT => Tmult_opp_left
+   | C_MULT_ASSOC_R => Tmult_assoc_r
+   | C_PLUS_ASSOC_R => Tplus_assoc_r
+   | C_PLUS_ASSOC_L => Tplus_assoc_l
+   | C_PLUS_PERMUTE => Tplus_permute
+   | C_PLUS_SYM => Tplus_sym
+   | C_RED0 => Tred_factor0
+   | C_RED1 => Tred_factor1
+   | C_RED2 => Tred_factor2
+   | C_RED3 => Tred_factor3
+   | C_RED4 => Tred_factor4
+   | C_RED5 => Tred_factor5
+   | C_RED6 => Tred_factor6
+   | C_MULT_ASSOC_REDUCED => Tmult_assoc_reduced
+   | C_MINUS => Tminus_def
+   | C_MULT_SYM => Tmult_sym
+  end.
+
+Theorem rewrite_stable : (s:step) (term_stable (rewrite s)).
+
+Induction s; Simpl; [
+  Intros; Apply apply_both_stable; Auto
+| Intros; Apply apply_left_stable; Auto
+| Intros; Apply apply_right_stable; Auto
+| Unfold term_stable; Intros; Elim H0; Apply H
+| Unfold term_stable; Auto
+| Exact Topp_plus_stable
+| Exact Topp_opp_stable
+| Exact Topp_mult_r_stable
+| Exact Topp_one_stable
+| Exact reduce_stable
+| Exact Tmult_plus_distr_stable
+| Exact Tmult_opp_left_stable
+| Exact Tmult_assoc_r_stable
+| Exact Tplus_assoc_r_stable
+| Exact Tplus_assoc_l_stable
+| Exact Tplus_permute_stable
+| Exact Tplus_sym_stable
+| Exact Tred_factor0_stable
+| Exact Tred_factor1_stable
+| Exact Tred_factor2_stable
+| Exact Tred_factor3_stable
+| Exact Tred_factor4_stable
+| Exact Tred_factor5_stable
+| Exact Tred_factor6_stable
+| Exact Tmult_assoc_reduced_stable
+| Exact Tminus_def_stable
+| Exact Tmult_sym_stable ].
+Save.
+
+(* \subsection{tactiques de résolution d'un but omega normalisé} 
+   Trace de la procédure 
+\subsubsection{Tactiques générant une contradiction}
+\paragraph{[O_CONSTANT_NOT_NUL]} *)
+
+Definition constant_not_nul [i:nat; h: hyps] :=
+  Cases (nth_hyps i h) of
+     (EqTerm (Tint ZERO) (Tint n)) =>
+	Case (eq_Z n ZERO) of
+	    h
+            absurd
+        end
+   | _ => h
+  end.
+
+Theorem constant_not_nul_valid : 
+  (i:nat) (valid_hyps (constant_not_nul i)).
+
+Unfold valid_hyps constant_not_nul; Intros;
+Generalize (nth_valid e i lp); (Simplify ()); Simpl; (Elim_eq_Z z0 ZERO); Auto;
+Simpl; Intros H1 H2; Elim H1; Symmetry; Auto.
+Save.   
+
+(* \paragraph{[O_CONSTANT_NEG]} *)
+
+Definition constant_neg [i:nat; h: hyps] :=
+   Cases (nth_hyps i h) of
+      (LeqTerm (Tint ZERO) (Tint (NEG n))) => absurd
+   | _ => h
+   end.
+
+Theorem constant_neg_valid : (i:nat) (valid_hyps (constant_neg i)).
+
+Unfold valid_hyps constant_neg; Intros;
+Generalize (nth_valid e i lp); (Simplify ()); Simpl; Unfold Zle; Simpl;
+Intros H1; Elim H1; [ Assumption | Trivial ].
+Save.   
+
+(* \paragraph{[NOT_EXACT_DIVIDE]} *)
+Definition not_exact_divide [k1,k2:Z; body:term; t:nat; i : nat; l:hyps] :=
+  Cases (nth_hyps i l) of
+      (EqTerm (Tint ZERO) b) =>
+         Case (eq_term
+	         (scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) b) of
+	   Cases (Zcompare k2 ZERO) of
+	     SUPERIEUR =>
+	       Cases (Zcompare k1 k2) of
+		 SUPERIEUR => absurd
+	       | _ => l
+	       end
+	   | _ => l
+           end
+	   l
+         end
+   | _ => l
+   end.
+
+Theorem not_exact_divide_valid : (k1,k2:Z; body:term; t:nat; i:nat) 
+	(valid_hyps (not_exact_divide k1 k2 body t i)).
+
+Unfold valid_hyps not_exact_divide; Intros; Generalize (nth_valid e i lp);
+(Simplify ());
+(Elim_eq_term '(scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2)))
+	     't1); Auto; 
+(Simplify ()); 
+Intro H2; Elim H2; Simpl; Elim (scalar_norm_add_stable t e); Simpl;
+Intro H4; Absurd `(interp_term e body)*k1+k2 = 0`; [
+   Apply OMEGA4; Assumption | Symmetry; Auto ].
+
+Save.
+
+(* \paragraph{[O_CONTRADICTION]} *)
+
+Definition contradiction [t: nat; i,j:nat;l:hyps] :=
+  Cases (nth_hyps i l) of
+    (LeqTerm  (Tint ZERO) b1) =>
+	Cases (nth_hyps j l) of 
+	  (LeqTerm  (Tint ZERO) b2) => 
+	     Cases (fusion_cancel t (Tplus b1 b2)) of
+	       (Tint k) =>
+		  Cases (Zcompare ZERO k) of
+	            SUPERIEUR => absurd
+	          | _ => l
+                  end
+             | _ => l
+             end
+         | _ => l 
+        end
+  | _ => l 
+  end.
+
+Theorem contradiction_valid : (t,i,j: nat) (valid_hyps (contradiction t i j)).
+
+Unfold valid_hyps contradiction; Intros t i j e l H;
+Generalize (nth_valid ? i ? H); Generalize (nth_valid ? j ? H);
+Case (nth_hyps i l); Auto; Intros t1 t2; Case t1; Auto; Intros z; Case z; Auto;
+Case (nth_hyps j l); Auto; Intros t3 t4; Case t3; Auto; Intros z'; Case z'; 
+Auto; Simpl; Intros H1 H2;
+Generalize (refl_equal Z (interp_term e (fusion_cancel t (Tplus t2 t4))));
+Pattern 2 3 (fusion_cancel t (Tplus t2 t4));
+Case (fusion_cancel t (Tplus t2 t4)); 
+Simpl; Auto; Intro k; Elim (fusion_cancel_stable t);
+Simpl; Intro E; Generalize (OMEGA2 ? ? H2 H1); Rewrite E; Case k; 
+Auto;Unfold Zle; Simpl; Intros p H3; Elim H3; Auto.
+
+Save.
+
+(* \paragraph{[O_NEGATE_CONTRADICT]} *)
+
+Definition negate_contradict [i1,i2:nat; h:hyps]:=
+  Cases (nth_hyps i1 h) of
+    (EqTerm (Tint ZERO) b1) =>
+	Cases (nth_hyps i2 h) of
+           (NeqTerm (Tint ZERO) b2) =>
+	      Cases (eq_term b1 b2) of
+	         true => absurd
+              |  false => h
+	    end
+        | _ => h
+        end
+  | (NeqTerm (Tint ZERO) b1) =>
+	Cases (nth_hyps i2 h) of
+           (EqTerm (Tint ZERO) b2) =>
+	      Cases (eq_term b1 b2) of
+	         true => absurd
+              |  false => h
+	    end
+        | _ => h
+        end
+  | _ => h
+  end.
+
+Theorem negate_contradict_valid :
+  (i,j:nat) (valid_hyps (negate_contradict i j)).
+
+Unfold valid_hyps negate_contradict; Intros i j e l H;
+Generalize (nth_valid ? i ? H); Generalize (nth_valid ? j ? H);
+Case (nth_hyps i l); Auto; Intros t1 t2; Case t1; Auto; Intros z; Case z; Auto;
+Case (nth_hyps j l); Auto; Intros t3 t4; Case t3; Auto; Intros z'; Case z'; 
+Auto; Simpl; Intros H1 H2; [
+  (Elim_eq_term t2 t4); Intro H3; [ Elim H1; Elim H3; Assumption | Assumption ]
+| (Elim_eq_term t2 t4); Intro H3; 
+    [ Elim H2; Rewrite H3; Assumption | Assumption ]].
+
+Save.
+
+(* \subsubsection{Tactiques générant une nouvelle équation} *)
+(* \paragraph{[O_SUM]}
+ C'est une oper2 valide mais elle traite plusieurs cas à la fois (suivant
+ les opérateurs de comparaison des deux arguments) d'où une
+ preuve un peu compliquée. On utilise quelques lemmes qui sont des 
+ généralisations des théorèmes utilisés par OMEGA. *)
+
+Definition sum [k1,k2: Z; trace: (list t_fusion); prop1,prop2:proposition]:=
+  Cases prop1 of
+    (EqTerm (Tint ZERO) b1) =>
+	Cases prop2 of
+          (EqTerm (Tint ZERO) b2) =>
+	    (EqTerm 
+	       (Tint ZERO) 
+	       (fusion trace 
+	               (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))))
+        | (LeqTerm (Tint ZERO) b2) =>
+	    Cases (Zcompare k2 ZERO) of
+	       SUPERIEUR =>
+		 (LeqTerm 
+		    (Tint ZERO) 
+		    (fusion trace 
+			 (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))))
+            | _ => TrueTerm
+           end
+       | _ => TrueTerm
+       end
+  | (LeqTerm (Tint ZERO) b1) =>
+      Cases (Zcompare k1 ZERO) of
+        SUPERIEUR =>
+	  Cases prop2 of
+	    (EqTerm (Tint ZERO) b2) =>
+	      (LeqTerm 
+		 (Tint ZERO) 
+		 (fusion trace 
+			 (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))))
+	  | (LeqTerm (Tint ZERO) b2) =>
+	       Cases (Zcompare k2 ZERO) of
+		  SUPERIEUR =>
+		    (LeqTerm 
+		       (Tint ZERO) 
+		       (fusion trace 
+			    (Tplus (Tmult b1 (Tint k1)) 
+                                   (Tmult b2 (Tint k2)))))
+	       | _ => TrueTerm
+	      end
+	 | _ => TrueTerm
+	 end
+     | _ => TrueTerm
+     end
+  | (NeqTerm (Tint ZERO) b1) =>
+       Cases prop2 of
+	 (EqTerm (Tint ZERO) b2) =>
+	    Case (eq_Z k1 ZERO) of
+	       TrueTerm
+	       (NeqTerm 
+		  (Tint ZERO) 
+		  (fusion trace 
+			  (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))))
+	    end
+      | _ => TrueTerm
+      end
+  | _ => TrueTerm
+  end.
+
+Theorem sum1 :
+  (a,b,c,d:Z) (`0 = a`) -> (`0 = b`) -> (`0 = a*c + b*d`).
+
+Intros; Elim H; Elim H0; Simpl; Auto.
+Save.
+  
+Theorem sum2 :
+  (a,b,c,d:Z)  (`0 <= d`) -> (`0 = a`) -> (`0 <= b`) ->(`0 <= a*c + b*d`).
+
+Intros; Elim H0; Simpl; Generalize H H1; Case b; Case d; 
+Unfold Zle; Simpl; Auto.  
+Save.
+
+Theorem sum3 :
+  (a,b,c,d:Z)  (`0 <= c`) -> (`0 <= d`) -> (`0 <= a`) -> (`0 <= b`) ->(`0 <= a*c + b*d`).
+
+Intros a b c d; Case a; Case b; Case c; Case d; Unfold Zle; Simpl; Auto. 
+Save.
+
+Theorem sum4 : (k:Z) (Zcompare k `0`)=SUPERIEUR -> (`0 <= k`).
+
+Intro; Case k; Unfold Zle; Simpl; Auto; Intros; Discriminate.  
+Save.
+
+Theorem sum5 :
+  (a,b,c,d:Z) (`c <> 0`) -> (`0 <> a`) -> (`0 = b`) -> (`0 <> a*c + b*d`).
+
+Intros a b c d H1 H2 H3; Elim H3; Simpl; Rewrite Zplus_sym;
+Simpl; Generalize H1 H2; Case a; Case c; Simpl; Intros; Try Discriminate;
+Assumption.
+Save.
+
+
+Theorem sum_valid : (k1,k2:Z; t:(list t_fusion)) (valid2 (sum k1 k2 t)).
+
+Unfold valid2; Intros k1 k2 t e p1 p2; Unfold sum; (Simplify ()); Simpl; Auto;
+Try (Elim (fusion_stable t)); Simpl; Intros; [
+  Apply sum1; Assumption
+| Apply sum2; Try Assumption; Apply sum4; Assumption
+| Rewrite Zplus_sym; Apply sum2; Try Assumption; Apply sum4; Assumption
+| Apply sum3; Try Assumption; Apply sum4; Assumption
+| (Elim_eq_Z k1 ZERO); Simpl; Auto; Elim (fusion_stable t); Simpl; Intros;
+  Unfold Zne; Apply sum5; Assumption].
+Save.
+
+(* \paragraph{[O_EXACT_DIVIDE]}
+   c'est une oper1 valide mais on préfère une substitution a ce point la *)
+
+Definition exact_divide [k:Z; body:term; t: nat; prop:proposition] :=
+   Cases prop of
+      (EqTerm (Tint ZERO) b) =>
+         Case (eq_term (scalar_norm t (Tmult body (Tint k))) b) of
+	   Case (eq_Z k ZERO) of
+	      TrueTerm
+	      (EqTerm (Tint ZERO) body)
+           end
+           TrueTerm
+         end
+   | _ => TrueTerm
+   end.
+
+Theorem exact_divide_valid :
+  (k:Z) (t:term) (n:nat) (valid1 (exact_divide k t n)).
+
+
+Unfold valid1 exact_divide; Intros k1 k2 t e p1; (Simplify ());Simpl; Auto;
+(Elim_eq_term  '(scalar_norm t (Tmult k2 (Tint k1))) 't1); Simpl; Auto;
+(Elim_eq_Z 'k1 'ZERO); Simpl; Auto;  Intros H1 H2; Elim H2; 
+Elim scalar_norm_stable; Simpl; Generalize H1; Case (interp_term e k2);
+Try Trivial; (Case k1; Simpl; [
+  Intros; Absurd `0 = 0`; Assumption
+| Intros p2 p3 H3 H4; Discriminate H4
+| Intros p2 p3 H3 H4; Discriminate H4 ]).
+
+Save.
+
+
+
+(* \paragraph{[O_DIV_APPROX]}
+  La preuve reprend le schéma de la précédente mais on
+  est sur une opération de type valid1 et non sur une opération terminale. *)
+
+Definition divide_and_approx [k1,k2:Z; body:term; t:nat; prop:proposition] :=
+  Cases prop of
+      (LeqTerm (Tint ZERO) b) =>
+         Case (eq_term
+                (scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) b) of
+	   Cases (Zcompare k1 ZERO) of
+	     SUPERIEUR =>
+	       Cases (Zcompare k1 k2) of
+		 SUPERIEUR =>(LeqTerm (Tint ZERO) body)
+	       | _ => prop
+	       end
+	   | _ => prop
+           end
+	   prop
+         end
+   | _ => prop
+   end.
+
+Theorem divide_and_approx_valid : (k1,k2:Z; body:term; t:nat) 
+	(valid1 (divide_and_approx k1 k2 body t)).
+
+Unfold valid1 divide_and_approx; Intros k1 k2 body t e p1;(Simplify ());
+(Elim_eq_term '(scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) 't1); (Simplify ()); Auto;  Intro E; Elim E; Simpl; 
+Elim (scalar_norm_add_stable t e); Simpl; Intro H1; 
+Apply Zmult_le_approx with 3 := H1; Assumption.
+Save.
+
+(* \paragraph{[MERGE_EQ]} *)
+
+Definition merge_eq [t: nat; prop1, prop2: proposition] :=
+  Cases prop1 of
+     (LeqTerm (Tint ZERO) b1) =>
+	Cases prop2 of
+     	  (LeqTerm (Tint ZERO) b2) =>
+             Case (eq_term b1 (scalar_norm t (Tmult b2 (Tint `-1`)))) of
+	        (EqTerm (Tint ZERO) b1)
+ 	       	TrueTerm
+	     end
+        | _ => TrueTerm
+	end
+  | _ => TrueTerm
+  end.
+
+Theorem merge_eq_valid : (n:nat) (valid2 (merge_eq n)).
+
+Unfold valid2 merge_eq; Intros n e p1 p2; (Simplify ()); Simpl; Auto;
+Elim (scalar_norm_stable n e); Simpl; Intros; Symmetry; 
+Apply OMEGA8 with 2 := H0; [ Assumption | Elim Zopp_one; Trivial ].
+Save.
+
+
+
+(* \paragraph{[O_CONSTANT_NUL]} *)
+
+Definition constant_nul [i:nat; h: hyps] :=
+  Cases (nth_hyps i h) of
+     (NeqTerm (Tint ZERO) (Tint ZERO)) => absurd
+   | _ => h
+  end.
+
+Theorem constant_nul_valid : 
+  (i:nat) (valid_hyps (constant_nul i)).
+
+Unfold valid_hyps constant_nul; Intros; Generalize (nth_valid e i lp);
+(Simplify ()); Simpl; Unfold Zne; Intro H1; Absurd `0=0`; Auto.
+Save.
+
+(* \paragraph{[O_STATE]} *)
+
+Definition state [m:Z;s:step; prop1,prop2:proposition] :=
+  Cases prop1 of
+     (EqTerm (Tint ZERO) b1) =>
+	Cases prop2 of
+	   (EqTerm (Tint ZERO) (Tplus b2 (Topp b3))) =>
+	      (EqTerm (Tint ZERO) (rewrite s (Tplus b1 (Tmult (Tplus (Topp b3) b2) (Tint m)))))
+	| _ => TrueTerm
+	end
+  | _ => TrueTerm
+  end.
+
+Theorem state_valid : (m:Z; s:step) (valid2 (state m s)).
+
+Unfold valid2; Intros m s e p1 p2; Unfold state; (Simplify ()); Simpl;Auto;
+Elim (rewrite_stable s e); Simpl; Intros H1 H2; Elim H1;
+Rewrite (Zplus_sym `-(interp_term e t5)` `(interp_term e t3)`);
+Elim H2; Simpl; Reflexivity.
+
+Save.
+
+(* \subsubsection{Tactiques générant plusieurs but}
+   \paragraph{[O_SPLIT_INEQ]} 
+   La seule pour le moment (tant que la normalisation n'est pas réfléchie). *)
+
+Definition split_ineq  [i,t: nat; f1,f2:hyps -> lhyps;  l:hyps] :=
+  Cases (nth_hyps i l) of
+    (NeqTerm  (Tint ZERO) b1) =>
+       (app (f1 (cons (LeqTerm (Tint ZERO) (add_norm t (Tplus b1 (Tint `-1`)))) l))
+            (f2 (cons (LeqTerm (Tint ZERO) 
+                               (scalar_norm_add t 
+	                         (Tplus (Tmult b1 (Tint `-1`)) (Tint `-1`))))
+                      l)))
+  | _ => (cons l (nil ?))
+  end.
+
+Theorem split_ineq_valid : 
+  (i,t: nat; f1,f2: hyps -> lhyps) 
+    (valid_list_hyps f1) ->(valid_list_hyps f2) -> 
+      (valid_list_hyps (split_ineq i t f1 f2)).
+
+Unfold valid_list_hyps split_ineq; Intros i t f1 f2 H1 H2 e lp H; 
+Generalize (nth_valid ? i ? H); 
+Case (nth_hyps i lp); Simpl; Auto; Intros t1 t2; Case t1; Simpl; Auto;
+Intros z; Case z; Simpl; Auto;
+Intro H3; Apply append_valid;Elim (OMEGA19 (interp_term e t2)) ;[
+  Intro H4; Left; Apply H1; Simpl; Elim (add_norm_stable t); Simpl; Auto
+| Intro H4; Right; Apply H2; Simpl; Elim (scalar_norm_add_stable t); 
+  Simpl; Auto
+| Generalize H3; Unfold Zne not; Intros E1 E2; Apply E1; Symmetry; Trivial ].
+Save.
+
+
+(* \subsection{La fonction de rejeu de la trace} *)
+Inductive t_omega : Set :=
+   (* n = 0 n!= 0 *)
+ | O_CONSTANT_NOT_NUL : nat -> t_omega
+ | O_CONSTANT_NEG : nat -> t_omega
+   (* division et approximation d'une équation *)
+ | O_DIV_APPROX : Z -> Z -> term -> nat -> t_omega -> nat -> t_omega
+   (* pas de solution car pas de division exacte (fin) *)
+ | O_NOT_EXACT_DIVIDE :  Z -> Z -> term -> nat -> nat -> t_omega
+   (* division exacte *)
+ | O_EXACT_DIVIDE : Z -> term -> nat -> t_omega -> nat -> t_omega
+ | O_SUM : Z -> nat -> Z -> nat -> (list t_fusion) -> t_omega -> t_omega
+ | O_CONTRADICTION : nat -> nat -> nat -> t_omega
+ | O_MERGE_EQ : nat -> nat -> nat -> t_omega -> t_omega
+ | O_SPLIT_INEQ : nat -> nat -> t_omega -> t_omega -> t_omega
+ | O_CONSTANT_NUL : nat -> t_omega 
+ | O_NEGATE_CONTRADICT : nat -> nat -> t_omega
+ | O_STATE : Z -> step -> nat -> nat -> t_omega -> t_omega.
+
+Syntactic Definition singleton :=  [a: hyps] (cons a (nil hyps)).
+
+Fixpoint execute_omega [t: t_omega] : hyps -> lhyps := 
+  [l : hyps] Cases t of
+   | (O_CONSTANT_NOT_NUL n) => (singleton (constant_not_nul n l))
+   | (O_CONSTANT_NEG n) => (singleton (constant_neg n l))
+   | (O_DIV_APPROX  k1 k2 body t cont n) =>
+       (execute_omega cont 
+	  (apply_oper_1 n (divide_and_approx k1 k2 body t) l))
+   | (O_NOT_EXACT_DIVIDE  k1 k2 body t i) =>
+       (singleton (not_exact_divide k1 k2 body t i l))
+   | (O_EXACT_DIVIDE k body t cont n) =>
+       (execute_omega cont (apply_oper_1 n (exact_divide k body t) l))
+   | (O_SUM k1 i1 k2 i2 t cont) =>
+       (execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2 t) l))
+   | (O_CONTRADICTION t i j) =>
+       (singleton (contradiction t i j l))
+   | (O_MERGE_EQ t i1 i2 cont) =>
+       (execute_omega cont (apply_oper_2 i1 i2 (merge_eq t) l))
+   | (O_SPLIT_INEQ t i cont1 cont2) =>
+       (split_ineq i t (execute_omega cont1) (execute_omega cont2) l)
+   | (O_CONSTANT_NUL i) => (singleton (constant_nul i l))
+   | (O_NEGATE_CONTRADICT i j) =>  (singleton (negate_contradict i j l))
+   | (O_STATE m s i1 i2 cont) =>
+       (execute_omega cont (apply_oper_2 i1 i2 (state m s) l))
+  end.
+
+Theorem omega_valid : (t: t_omega) (valid_list_hyps (execute_omega t)).
+
+Induction t; Simpl; [
+  Unfold valid_list_hyps; Simpl; Intros; Left; 
+  Apply (constant_not_nul_valid n e lp H)
+| Unfold valid_list_hyps; Simpl; Intros; Left; 
+  Apply (constant_neg_valid n e lp H)
+| Unfold valid_list_hyps valid_hyps; Intros k1 k2 body n t' Ht' m e lp H; 
+  Apply Ht';
+  Apply (apply_oper_1_valid m (divide_and_approx k1 k2 body n)
+	  (divide_and_approx_valid k1 k2 body n) e lp H)
+| Unfold valid_list_hyps; Simpl; Intros; Left; 
+  Apply (not_exact_divide_valid z z0 t0 n n0 e lp H)
+| Unfold valid_list_hyps valid_hyps; Intros k body n t' Ht' m e lp H; 
+  Apply Ht';
+  Apply (apply_oper_1_valid m (exact_divide k body n)
+	  (exact_divide_valid k body n) e lp H)
+| Unfold valid_list_hyps valid_hyps; Intros k1 i1 k2 i2 trace t' Ht' e lp H;
+  Apply Ht'; 
+  Apply (apply_oper_2_valid i1 i2 (sum k1 k2 trace) 
+	  (sum_valid k1 k2 trace) e lp H)
+| Unfold valid_list_hyps; Simpl; Intros; Left; 
+  Apply (contradiction_valid n n0 n1 e lp H)
+| Unfold valid_list_hyps valid_hyps; Intros trace i1 i2 t' Ht' e lp H; 
+  Apply Ht';
+  Apply (apply_oper_2_valid i1 i2 (merge_eq trace) 
+          (merge_eq_valid trace) e lp H) 
+| Intros t' i k1 H1 k2 H2; Unfold valid_list_hyps; Simpl; Intros e lp H;
+  Apply (split_ineq_valid i t' (execute_omega k1) (execute_omega k2) 
+	 H1 H2 e lp H)
+| Unfold valid_list_hyps; Simpl; Intros i e lp H; Left; 
+  Apply (constant_nul_valid i e lp H)
+| Unfold valid_list_hyps; Simpl; Intros i j e lp H; Left; 
+  Apply (negate_contradict_valid i j e lp H)
+| Unfold valid_list_hyps valid_hyps; Intros m s i1 i2 t' Ht' e lp H; Apply Ht';
+  Apply (apply_oper_2_valid i1 i2 (state m s) (state_valid m s) e lp H)
+].
+Save.
+
+
+(* \subsection{Les opérations globales sur le but} 
+   \subsubsection{Normalisation} *)
+
+Definition move_right [s: step; p:proposition] :=
+  Cases p of
+     (EqTerm t1 t2) => (EqTerm (Tint ZERO) (rewrite s (Tplus t1 (Topp t2))))
+   | (LeqTerm t1 t2) => (LeqTerm (Tint ZERO) (rewrite s (Tplus t2 (Topp t1))))
+   | (GeqTerm t1 t2) => (LeqTerm (Tint ZERO) (rewrite s (Tplus t1 (Topp t2))))
+   | (LtTerm t1 t2) =>
+        (LeqTerm (Tint ZERO)
+	         (rewrite s (Tplus (Tplus t2 (Tint `-1`)) (Topp t1))))
+   | (GtTerm t1 t2) => 
+        (LeqTerm (Tint ZERO)
+                 (rewrite s (Tplus (Tplus t1 (Tint `-1`)) (Topp t2))))
+   | (NeqTerm t1 t2) => (NeqTerm (Tint ZERO) (rewrite s (Tplus t1 (Topp t2))))
+   | p => p
+  end.
+
+Theorem Zne_left_2 : (x,y:Z)(Zne x y)->(Zne `0` `x+(-y)`).
+Unfold Zne not; Intros x y H1 H2; Apply H1; Apply (Zsimpl_plus_l `-y`);
+Rewrite Zplus_sym; Elim H2; Rewrite Zplus_inverse_l; Trivial.
+Save.
+
+Theorem move_right_valid : (s: step) (valid1 (move_right s)).
+
+Unfold valid1 move_right; Intros s e p; (Simplify ()); Simpl;
+Elim (rewrite_stable s e); Simpl; [
+  Symmetry; Apply Zegal_left; Assumption
+| Intro; Apply Zle_left; Assumption 
+| Intro; Apply Zge_left; Assumption
+| Intro; Apply Zgt_left; Assumption
+| Intro; Apply Zlt_left; Assumption
+| Intro; Apply Zne_left_2; Assumption
+].
+Save.
+
+Definition do_normalize [i:nat; s: step] := (apply_oper_1 i (move_right s)).
+
+Theorem do_normalize_valid : (i:nat; s:step) (valid_hyps (do_normalize i s)).
+
+Intros; Unfold do_normalize; Apply apply_oper_1_valid; Apply move_right_valid.
+Save.
+
+Fixpoint do_normalize_list [l:(list step)] : nat -> hyps -> hyps := 
+  [i:nat; h:hyps] Cases l of
+    (cons s l') => (do_normalize_list l' (S i) (do_normalize i s h))
+  | nil => h
+  end.
+
+Theorem do_normalize_list_valid : 
+  (l:(list step); i:nat) (valid_hyps (do_normalize_list l i)).
+
+Induction l; Simpl; Unfold valid_hyps; [
+  Auto
+| Intros a l' Hl' i e lp H; Unfold valid_hyps in Hl'; Apply Hl';
+  Apply (do_normalize_valid i a e lp); Assumption ].
+Save.
+
+Theorem normalize_goal :
+  (s: (list step); env : (list Z); l: hyps)
+    (interp_goal env (do_normalize_list s O l)) -> 
+      (interp_goal env l).
+
+Intros; Apply valid_goal with 2:=H; Apply do_normalize_list_valid.
+Save.
+
+(* \subsubsection{Exécution de la trace} *)
+
+Theorem execute_goal :
+  (t : t_omega; env : (list Z); l: hyps)
+    (interp_list_goal env (execute_omega t l)) -> (interp_goal env l).
+
+Intros; Apply (goal_valid (execute_omega t) (omega_valid t) env l H).
+Save.
+
+
+Theorem append_goal :
+  (e: (list Z)) (l1,l2:lhyps)
+     (interp_list_goal e l1) /\ (interp_list_goal e l2) ->
+     (interp_list_goal e (app l1 l2)).
+
+Intros e; Induction l1; [
+  Simpl; Intros l2 (H1, H2); Assumption
+| Simpl; Intros h1 t1 HR l2 ((H1 , H2), H3) ; Split; Auto].
+
+
+Save.
+
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
new file mode 100644
index 000000000..4c8dcca1b
--- /dev/null
+++ b/contrib/romega/const_omega.ml
@@ -0,0 +1,256 @@
+(*************************************************************************
+
+   PROJET RNRT Calife - 2001
+   Author: Pierre Crégut - France Télécom R&D
+   Licence : LGPL version 2.1
+
+ *************************************************************************)
+
+let module_refl_name = "ReflOmegaCore"
+let module_refl_path = ["Scratch"; module_refl_name]
+
+type result = 
+   Kvar of string
+ | Kapp of string * Term.constr list
+ | Kimp of Term.constr * Term.constr
+ | Kufo;;
+
+let destructurate t =
+  let c, args = Reduction.whd_stack t in
+  match Term.kind_of_term c, args with
+    | Term.IsConst (sp,_), args ->
+	Kapp (Names.string_of_id
+		(Names.basename (Global.sp_of_global (Term.ConstRef sp))),args)
+    | Term.IsMutConstruct (csp,_) , args ->
+	Kapp (Names.string_of_id
+		(Names.basename (Global.sp_of_global (Term.ConstructRef csp))),
+	      args)
+    | Term.IsMutInd (isp,_), args ->
+	Kapp (Names.string_of_id
+		(Names.basename (Global.sp_of_global (Term.IndRef isp))),args)
+    | Term.IsVar id,[] -> Kvar(Names.string_of_id id)
+    | Term.IsProd (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
+    | Term.IsProd (Names.Name _,_,_),[] ->
+	Util.error "Omega: Not a quantifier-free goal"
+    | _ -> Kufo
+
+exception Destruct
+
+let dest_const_apply t = 
+  let f,args = Reduction.whd_stack t in
+  let ref = 
+  match Term.kind_of_term f with 
+    | Term.IsConst (sp,_)         -> Term.ConstRef sp
+    | Term.IsMutConstruct (csp,_) -> Term.ConstructRef csp
+    | Term.IsMutInd (isp,_)       -> Term.IndRef isp
+    | _ -> raise Destruct
+  in
+  Names.basename (Global.sp_of_global ref), args
+
+let recognize_number t =
+  let rec loop t =
+    let f,l = dest_const_apply t in
+    match Names.string_of_id f,l with
+       "xI",[t] -> 1 + 2 * loop t
+     | "xO",[t] -> 2 * loop t 
+     | "xH",[] -> 1
+     | _ -> failwith "not a number" in
+  let f,l = dest_const_apply t in
+    match Names.string_of_id f,l with
+       "POS",[t] -> loop t | "NEG",[t] -> - (loop t) | "ZERO",[] -> 0
+     | _ -> failwith "not a number";;
+
+let constant dir s =
+  try
+    Declare.global_absolute_reference
+      (Names.make_path (List.map Names.id_of_string dir)
+                       (Names.id_of_string s) Names.CCI)
+  with e -> print_endline (String.concat "." dir); print_endline s; 
+            raise e
+
+let coq_xH = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "xH")
+let coq_xO = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "xO")
+let coq_xI = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "xI")
+let coq_ZERO = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "ZERO")
+let coq_POS = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "POS")
+let coq_NEG = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "NEG")
+let coq_Z = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "Z")
+let coq_relation = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "relation")
+let coq_SUPERIEUR = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "SUPERIEUR")
+let coq_INFEEIEUR = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "INFERIEUR")
+let coq_EGAL = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "EGAL")
+let coq_Zplus = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "Zplus")
+let coq_Zmult = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "Zmult")
+let coq_Zopp = lazy (constant ["Coq"; "ZArith"; "fast_integer"] "Zopp")
+
+(* auxiliaires zarith *)
+let coq_Zminus = lazy (constant ["Coq"; "ZArith"; "zarith_aux"] "Zminus")
+let coq_Zs = lazy (constant ["Coq"; "ZArith"; "zarith_aux"] "Zs")
+let coq_Zgt = lazy (constant ["Coq"; "ZArith"; "zarith_aux"] "Zgt")
+let coq_Zle = lazy (constant ["Coq"; "ZArith"; "zarith_aux"] "Zle")
+let coq_inject_nat = lazy (constant ["Coq"; "ZArith"; "zarith_aux"] "inject_nat")
+
+(* Peano *)
+let coq_le = lazy(constant ["Init"; "Peano"] "le")
+let coq_gt = lazy(constant ["Init"; "Peano"] "gt")
+
+(* Datatypes *)
+let coq_nat = lazy(constant ["Coq"; "Init"; "Datatypes"] "nat")
+let coq_S = lazy(constant ["Coq"; "Init"; "Datatypes"] "S")
+let coq_O = lazy(constant ["Coq"; "Init"; "Datatypes"] "O")
+
+(* Minus *)
+let coq_minus = lazy(constant ["Arith"; "Minus"] "minus")
+
+(* Logic *)
+let coq_eq = lazy(constant ["Init"; "Logic"] "eq")
+let coq_refl_equal = lazy(constant ["Coq"; "Init"; "Logic"] "refl_equal")
+let coq_and = lazy(constant ["Coq"; "Init"; "Logic"] "and")
+let coq_not = lazy(constant ["Coq"; "Init"; "Logic"] "not")
+let coq_or = lazy(constant ["Coq"; "Init"; "Logic"] "or")
+let coq_ex = lazy(constant ["Coq"; "Init"; "Logic"] "ex")
+
+(* Lists *)
+let coq_cons =  lazy (constant ["Coq"; "Lists"; "PolyList"] "cons")
+let coq_nil =  lazy (constant ["Coq"; "Lists"; "PolyList"] "nil")
+
+let coq_t_nat = lazy (constant module_refl_path "Tint")
+let coq_t_plus = lazy (constant module_refl_path "Tplus")
+let coq_t_mult = lazy (constant module_refl_path "Tmult")
+let coq_t_opp = lazy (constant module_refl_path "Topp")
+let coq_t_minus = lazy (constant module_refl_path "Tminus")
+let coq_t_var = lazy (constant module_refl_path "Tvar")
+let coq_t_equal = lazy (constant module_refl_path "EqTerm")
+let coq_t_leq = lazy (constant module_refl_path "LeqTerm")
+let coq_t_geq = lazy (constant module_refl_path "GeqTerm")
+let coq_t_lt = lazy (constant module_refl_path "LtTerm")
+let coq_t_gt = lazy (constant module_refl_path "GtTerm")
+let coq_t_neq = lazy (constant module_refl_path "NeqTerm")
+
+let coq_proposition = lazy (constant module_refl_path "proposition")
+let coq_interp_sequent = lazy (constant module_refl_path "interp_goal")
+let coq_normalize_sequent = lazy (constant module_refl_path "normalize_goal")
+let coq_execute_sequent = lazy (constant module_refl_path "execute_goal")
+let coq_sequent_to_hyps = lazy (constant module_refl_path "goal_to_hyps")
+
+(* Constructors for shuffle tactic *)
+let coq_t_fusion =  lazy (constant module_refl_path "t_fusion")
+let coq_f_equal =  lazy (constant module_refl_path "F_equal")
+let coq_f_cancel =  lazy (constant module_refl_path "F_cancel")
+let coq_f_left =  lazy (constant module_refl_path "F_left")
+let coq_f_right =  lazy (constant module_refl_path "F_right")
+
+(* Constructors for reordering tactics *)
+let coq_step = lazy (constant module_refl_path "step")
+let coq_c_do_both = lazy (constant module_refl_path "C_DO_BOTH")
+let coq_c_do_left = lazy (constant module_refl_path "C_LEFT")
+let coq_c_do_right = lazy (constant module_refl_path "C_RIGHT")
+let coq_c_do_seq = lazy (constant module_refl_path "C_SEQ")
+let coq_c_nop = lazy (constant module_refl_path "C_NOP")
+let coq_c_opp_plus = lazy (constant module_refl_path "C_OPP_PLUS")
+let coq_c_opp_opp = lazy (constant module_refl_path "C_OPP_OPP")
+let coq_c_opp_mult_r = lazy (constant module_refl_path "C_OPP_MULT_R")
+let coq_c_opp_one = lazy (constant module_refl_path "C_OPP_ONE")
+let coq_c_reduce = lazy (constant module_refl_path "C_REDUCE")
+let coq_c_mult_plus_distr = lazy (constant module_refl_path "C_MULT_PLUS_DISTR")
+let coq_c_opp_left = lazy (constant module_refl_path "C_MULT_OPP_LEFT")
+let coq_c_mult_assoc_r = lazy (constant module_refl_path "C_MULT_ASSOC_R")
+let coq_c_plus_assoc_r = lazy (constant module_refl_path "C_PLUS_ASSOC_R")
+let coq_c_plus_assoc_l = lazy (constant module_refl_path "C_PLUS_ASSOC_L")
+let coq_c_plus_permute = lazy (constant module_refl_path "C_PLUS_PERMUTE")
+let coq_c_plus_sym = lazy (constant module_refl_path "C_PLUS_SYM")
+let coq_c_red0 = lazy (constant module_refl_path "C_RED0")
+let coq_c_red1 = lazy (constant module_refl_path "C_RED1")
+let coq_c_red2 = lazy (constant module_refl_path "C_RED2")
+let coq_c_red3 = lazy (constant module_refl_path "C_RED3")
+let coq_c_red4 = lazy (constant module_refl_path "C_RED4")
+let coq_c_red5 = lazy (constant module_refl_path "C_RED5")
+let coq_c_red6 = lazy (constant module_refl_path "C_RED6")
+let coq_c_mult_opp_left = lazy (constant module_refl_path "C_MULT_OPP_LEFT")
+let coq_c_mult_assoc_reduced = 
+  lazy (constant module_refl_path "C_MULT_ASSOC_REDUCED")
+let coq_c_minus = lazy (constant module_refl_path "C_MINUS")
+let coq_c_mult_sym = lazy (constant module_refl_path "C_MULT_SYM")
+
+let coq_s_constant_not_nul = lazy (constant module_refl_path "O_CONSTANT_NOT_NUL")
+let coq_s_constant_neg = lazy (constant module_refl_path "O_CONSTANT_NEG")
+let coq_s_div_approx = lazy (constant module_refl_path "O_DIV_APPROX")
+let coq_s_not_exact_divide = lazy (constant module_refl_path "O_NOT_EXACT_DIVIDE")
+let coq_s_exact_divide = lazy (constant module_refl_path "O_EXACT_DIVIDE")
+let coq_s_sum = lazy (constant module_refl_path "O_SUM")
+let coq_s_state = lazy (constant module_refl_path "O_STATE")
+let coq_s_contradiction = lazy (constant module_refl_path "O_CONTRADICTION")
+let coq_s_merge_eq = lazy (constant module_refl_path "O_MERGE_EQ")
+let coq_s_split_ineq =lazy (constant module_refl_path "O_SPLIT_INEQ")
+let coq_s_constant_nul =lazy (constant module_refl_path "O_CONSTANT_NUL")
+let coq_s_negate_contradict =lazy (constant module_refl_path "O_NEGATE_CONTRADICT")
+
+(* \subsection{Construction d'expressions} *)
+
+
+let mk_var v = Term.mkVar (Names.id_of_string v)
+let mk_plus t1 t2 = Term.mkApp (Lazy.force coq_Zplus,[|  t1; t2 |])
+let mk_times t1 t2 = Term.mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
+let mk_minus t1 t2 = Term.mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
+let mk_eq t1 t2 = Term.mkApp (Lazy.force coq_eq, [| Lazy.force coq_Z; t1; t2 |])
+let mk_le t1 t2 = Term.mkApp (Lazy.force coq_Zle, [|t1; t2 |])
+let mk_gt t1 t2 = Term.mkApp (Lazy.force coq_Zgt, [|t1; t2 |])
+let mk_inv t = Term.mkApp (Lazy.force coq_Zopp, [|t |])
+let mk_and t1 t2 =  Term.mkApp (Lazy.force coq_and, [|t1; t2 |])
+let mk_or t1 t2 =  Term.mkApp (Lazy.force coq_or, [|t1; t2 |])
+let mk_not t = Term.mkApp (Lazy.force coq_not, [|t |])
+let mk_eq_rel t1 t2 = Term.mkApp (Lazy.force coq_eq, [|
+				Lazy.force coq_relation; t1; t2 |])
+let mk_inj t = Term.mkApp (Lazy.force coq_inject_nat, [|t |])
+
+
+let do_left t = 
+  if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop
+  else Term.mkApp (Lazy.force coq_c_do_left, [|t |] )
+
+let do_right t = 
+  if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop
+  else Term.mkApp (Lazy.force coq_c_do_right, [|t |])
+
+let do_both t1 t2 = 
+  if t1 = Lazy.force coq_c_nop then do_right t2
+  else if t2 = Lazy.force coq_c_nop then do_left t1
+  else Term.mkApp (Lazy.force coq_c_do_both , [|t1; t2 |])
+
+let do_seq t1 t2 =
+  if t1 = Lazy.force coq_c_nop then t2
+  else if t2 = Lazy.force coq_c_nop then t1
+  else Term.mkApp (Lazy.force coq_c_do_seq, [|t1; t2 |])
+  
+let rec do_list = function
+  | [] -> Lazy.force coq_c_nop
+  | [x] -> x
+  | (x::l) -> do_seq x (do_list l)
+
+				 
+let mk_integer n =
+  let rec loop n = 
+    if n=1 then Lazy.force coq_xH else 
+      Term.mkApp ((if n mod 2 = 0 then Lazy.force coq_xO else Lazy.force coq_xI),
+		 [| loop (n/2) |]) in
+    
+    if n = 0 then Lazy.force coq_ZERO 
+    else Term.mkApp ((if n > 0 then Lazy.force coq_POS else Lazy.force coq_NEG),
+		     [| loop (abs n) |])
+
+let mk_Z = mk_integer
+
+let rec mk_nat = function
+  | 0 -> Lazy.force coq_O
+  | n -> Term.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |])
+
+let mk_list typ l =
+  let rec loop = function
+    | [] ->
+	Term.mkApp (Lazy.force coq_nil, [|typ|])
+    | (step :: l) -> 
+	Term.mkApp (Lazy.force coq_cons, [|typ; step; loop l |]) in
+  loop l
+
+let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l
+
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
new file mode 100644
index 000000000..3974ab39c
--- /dev/null
+++ b/contrib/romega/refl_omega.ml
@@ -0,0 +1,855 @@
+(*************************************************************************
+
+   PROJET RNRT Calife - 2001
+   Author: Pierre Crégut - France Télécom R&D
+   Licence : LGPL version 2.1
+
+ *************************************************************************)
+
+open Const_omega
+
+
+(* \section{Utilitaires} *)
+
+let debug = ref false 
+
+let (>>) = Tacticals.tclTHEN
+
+let index t = 
+  let rec loop i = function
+    | (u::l) -> if u = t then i else loop (i+1) l
+    | [] -> raise Not_found in
+  loop 0
+
+let mkApp = Term.mkApp
+
+(* \section{Formules réifiables} *)
+type oformula =
+  | Oplus of oformula * oformula
+  | Ominus of oformula * oformula
+  | Oinv of  oformula
+  | Otimes of oformula * oformula
+  | Oatom of  int
+  | Oz of int
+  | Oufo of oformula
+
+let rec oprint = function 
+  | Oplus(t1,t2) -> 
+      print_string "("; oprint t1; print_string "+"; 
+      oprint t2; print_string ")"
+  | Ominus(t1,t2) -> 
+      print_string "("; oprint t1; print_string "-"; 
+      oprint t2; print_string ")"
+  | Oinv t -> print_string "~"; oprint t
+  | Otimes (t1,t2) -> 
+      print_string "("; oprint t1; print_string "*"; 
+      oprint t2; print_string ")"
+  | Oatom i ->print_string "V";  print_int i
+  | Oz i -> print_int i
+  | Oufo f -> print_string "?"
+
+(* \section{Tables} *)
+
+let get_hyp env_hyp id = 
+  try index id env_hyp 
+  with Not_found -> failwith ("get_hyp " ^ string_of_int id)
+
+let tag_equation,tag_of_equation, clear_tags  =
+  let l = ref ([]:(int * Names.identifier) list) in
+  (fun id h -> l := (h,id):: !l),
+  (fun h -> try List.assoc h !l with Not_found-> failwith "tag_hypothesis"),
+  (fun () -> l := [])
+
+let add_atom t env =
+  try index t env, env
+  with Not_found ->  List.length env, (env@[t])
+
+let get_atom v env = 
+  try List.nth v env with _ -> failwith "get_atom"
+
+(* compilation des environnements *)
+
+let intern_id, intern_id_force, unintern_id, clear_intern =
+  let c = ref 0 in
+  let l = ref [] in
+  (fun t -> 
+     try List.assoc t !l 
+     with Not_found -> incr c; let v = !c in l := (t,v)::!l; v),
+  (fun t v -> l := (t,v) :: !l),
+  (fun i ->
+    let rec loop = function 
+	[] -> failwith "unintern" 
+      | ((t,j)::l) -> if i = j then t else loop l in
+    loop !l),
+  (fun () -> c := 0; l := [])
+
+(* Le poids d'un terme : fondamental pour classer les variables *)
+
+let rec weight = function
+  | Oatom _ as c -> intern_id c
+  | Oz _ -> -1
+  | Oinv c -> weight c
+  | Otimes(c,_) -> weight c
+  | Oplus _ -> failwith "weight"
+  | Ominus _ -> failwith "weight minus"
+  | Oufo _ -> -1
+
+(* \section{Passage entre oformules et 
+               représentation interne de Omega} *)
+
+(* \subsection{Oformula vers Omega} *)
+
+let compile name kind = 
+  let rec loop accu = function
+    | Oplus(Otimes(v,Oz n),r) -> 
+	loop ({Omega.v=intern_id v; Omega.c=n} :: accu) r
+    | Oz n ->
+	let id = Omega.new_id () in
+	tag_equation name id;
+	{Omega.kind = kind; Omega.body = List.rev accu; 
+	 Omega.constant = n; Omega.id = id}
+    | t -> print_string "CO"; oprint t; failwith "compile_equation" in
+  loop []
+
+(* \subsection{Omega vers Oformula} *)
+
+let rec decompile af = 
+  let rec loop = function
+    | ({Omega.v=v; Omega.c=n}::r) -> Oplus(Otimes(unintern_id v,Oz n),loop r) 
+    | [] -> Oz af.Omega.constant in
+  loop af.Omega.body
+
+(* \subsection{Oformula vers COQ reel} *)
+
+let rec coq_of_formula env t =
+  let rec loop = function
+  | Oplus (t1,t2) -> mkApp(Lazy.force coq_Zplus, [| loop t1; loop t2 |])
+  | Oinv t -> mkApp(Lazy.force coq_Zopp, [| loop t |])
+  | Otimes(t1,t2) -> mkApp(Lazy.force coq_Zmult, [| loop t1; loop t2 |])
+  | Oz v ->  mk_Z v
+  | Oufo t -> loop t
+  | Oatom i -> get_atom env i
+  | Ominus(t1,t2) -> mkApp(Lazy.force coq_Zminus, [| loop t1; loop t2 |]) in
+  loop t
+
+(* \subsection{Oformula vers COQ reifié} *)
+
+let rec val_of_formula = function
+  | Oplus (t1,t2) ->
+      mkApp(Lazy.force coq_t_plus, [| val_of_formula t1; val_of_formula t2 |])
+  | Oinv t ->
+      mkApp(Lazy.force coq_t_opp, [| val_of_formula t |])
+  | Otimes(t1,t2) ->
+      mkApp(Lazy.force coq_t_mult, [| val_of_formula t1; val_of_formula t2 |])
+  | Oz v ->  mkApp (Lazy.force coq_t_nat, [| mk_Z v |])
+  | Oufo t -> val_of_formula t
+  | Oatom i -> mkApp(Lazy.force coq_t_var, [| mk_nat i |])
+  | Ominus(t1,t2) ->
+      mkApp(Lazy.force coq_t_minus, [| val_of_formula t1; val_of_formula t2 |])
+
+(* \subsection{Omega vers COQ réifié} *)
+
+let val_of body constant = 
+  let coeff_constant = 
+    mkApp(Lazy.force coq_t_nat, [| mk_Z constant |]) in
+  let mk_coeff {Omega.c=c; Omega.v=v} t =
+    let coef = mkApp(Lazy.force coq_t_mult,
+		     [|val_of_formula (unintern_id v );
+		       mkApp(Lazy.force coq_t_nat, [| mk_Z c |]) |]) in
+    mkApp(Lazy.force coq_t_plus, [|coef; t |]) in
+  List.fold_right mk_coeff body coeff_constant
+
+(* \section{Opérations sur les équations}
+Ces fonctions préparent les traces utilisées par la tactique réfléchie
+pour faire des opérations de normalisation sur les équations.  *)
+
+(* \subsection{Multiplication par un scalaire} *)
+let rec scalar n = function
+   Oplus(t1,t2) -> 
+     let tac1,t1' = scalar  n t1 and 
+         tac2,t2' = scalar  n t2 in
+     do_list [Lazy.force coq_c_mult_plus_distr; do_both tac1 tac2], 
+     Oplus(t1',t2')
+ | Oinv t ->
+     do_list [Lazy.force coq_c_mult_opp_left], Otimes(t,Oz(-n))
+ | Otimes(t1,Oz x) -> 
+     do_list [Lazy.force coq_c_mult_assoc_reduced], Otimes(t1,Oz (n*x))
+ | Otimes(t1,t2) -> 
+     Util.error "Omega: Can't solve a goal with non-linear products"
+ | (Oatom _ as t) -> do_list [], Otimes(t,Oz n)
+ | Oz i -> do_list [Lazy.force coq_c_reduce],Oz(n*i)
+ | (Oufo _ as t)-> do_list [], Oufo (Otimes(t,Oz n))
+ | Ominus _ -> failwith "scalar minus"
+
+(* \subsection{Propagation de l'inversion} *)
+let rec negate = function
+   Oplus(t1,t2) -> 
+     let tac1,t1' = negate t1 and 
+         tac2,t2' = negate t2 in
+     do_list [Lazy.force coq_c_opp_plus ; (do_both tac1 tac2)],
+     Oplus(t1',t2')
+ | Oinv t ->
+     do_list [Lazy.force coq_c_opp_opp], t
+ | Otimes(t1,Oz x) -> 
+     do_list [Lazy.force coq_c_opp_mult_r], Otimes(t1,Oz (-x))
+ | Otimes(t1,t2) -> 
+     Util.error "Omega: Can't solve a goal with non-linear products"
+ | (Oatom _ as t) ->
+     do_list [Lazy.force coq_c_opp_one], Otimes(t,Oz(-1))
+ | Oz i -> do_list [Lazy.force coq_c_reduce] ,Oz(-i)
+ | Oufo c -> do_list [], Oufo (Oinv c)
+ | Ominus _ -> failwith "negate minus"
+
+let rec norm l = (List.length l)
+
+(* \subsection{Mélange (fusion) de deux équations} *)
+
+let rec shuffle_path k1 e1 k2 e2 =
+  let rec loop = function
+      (({Omega.c=c1;Omega.v=v1}::l1) as l1'),
+      (({Omega.c=c2;Omega.v=v2}::l2) as l2') ->
+	if v1 = v2 then
+          if k1*c1 + k2 * c2 = 0 then (
+            Lazy.force coq_f_cancel :: loop (l1,l2))
+          else (
+            Lazy.force coq_f_equal :: loop (l1,l2) )
+	else if v1 > v2 then (
+	  Lazy.force coq_f_left :: loop(l1,l2'))
+	else (
+	  Lazy.force coq_f_right :: loop(l1',l2))
+    | ({Omega.c=c1;Omega.v=v1}::l1), [] -> 
+	  Lazy.force coq_f_left :: loop(l1,[])
+    | [],({Omega.c=c2;Omega.v=v2}::l2) -> 
+	  Lazy.force coq_f_right :: loop([],l2)
+    | [],[] -> flush stdout; [] in
+  mk_shuffle_list (loop (e1,e2))
+
+let rec shuffle (t1,t2) = 
+  match t1,t2 with
+    Oplus(l1,r1), Oplus(l2,r2) ->
+      if weight l1 > weight l2 then 
+	let l_action,t' = shuffle (r1,t2) in
+	do_list [Lazy.force coq_c_plus_assoc_r;do_right l_action], Oplus(l1,t')
+      else 
+	let l_action,t' = shuffle (t1,r2) in
+	do_list [Lazy.force coq_c_plus_permute;do_right l_action], Oplus(l2,t')
+  | Oplus(l1,r1), t2 -> 
+      if weight l1 > weight t2 then
+        let (l_action,t') = shuffle  (r1,t2) in
+	do_list [Lazy.force coq_c_plus_assoc_r;do_right l_action],Oplus(l1, t')
+      else do_list [Lazy.force coq_c_plus_sym], Oplus(t2,t1)
+  | t1,Oplus(l2,r2) -> 
+      if weight l2 > weight t1 then
+        let (l_action,t') = shuffle (t1,r2) in
+	do_list [Lazy.force coq_c_plus_permute;do_right l_action], Oplus(l2,t')
+      else do_list [],Oplus(t1,t2)
+  | Oz t1,Oz t2 ->
+      do_list [Lazy.force coq_c_reduce], Oz(t1+t2)
+  | t1,t2 ->
+      if weight t1 < weight t2 then
+	do_list [Lazy.force coq_c_plus_sym], Oplus(t2,t1)
+      else do_list [],Oplus(t1,t2)
+
+(* \subsection{Fusion avec réduction} *)
+let shrink_pair f1 f2 =
+  begin match f1,f2 with
+     Oatom v,Oatom _ -> 
+       Lazy.force coq_c_red1, Otimes(Oatom v,Oz 2)
+   | Oatom v, Otimes(_,c2) -> 
+       Lazy.force coq_c_red2, Otimes(Oatom v,Oplus(c2,Oz 1))
+   | Otimes (v1,c1),Oatom v -> 
+       Lazy.force coq_c_red3, Otimes(Oatom v,Oplus(c1,Oz 1))
+   | Otimes (Oatom v,c1),Otimes (v2,c2) ->
+       Lazy.force coq_c_red4, Otimes(Oatom v,Oplus(c1,c2))
+   | t1,t2 -> 
+       oprint t1; print_newline (); oprint t2; print_newline (); 
+       flush Pervasives.stdout; Util.error "shrink.1"
+  end
+
+(* \subsection{Calcul d'une sous formule constante} *)
+let reduce_factor = function
+   Oatom v ->
+     let r = Otimes(Oatom v,Oz 1) in
+       [Lazy.force coq_c_red0],r
+  | Otimes(Oatom v,Oz n) as f -> [],f
+  | Otimes(Oatom v,c) ->
+      let rec compute = function
+          Oz n -> n
+	| Oplus(t1,t2) -> compute t1 + compute t2 
+	| _ -> Util.error "condense.1" in
+	[Lazy.force coq_c_reduce], Otimes(Oatom v,Oz(compute c))
+  | t -> Util.error "reduce_factor.1"
+
+(* \subsection{Réordonancement} *)
+
+let rec condense = function
+    Oplus(f1,(Oplus(f2,r) as t)) ->
+      if weight f1 = weight f2 then begin
+	let shrink_tac,t = shrink_pair f1 f2 in
+	let assoc_tac = Lazy.force coq_c_plus_assoc_l in
+	let tac_list,t' = condense (Oplus(t,r)) in
+	assoc_tac :: do_left (do_list [shrink_tac]) :: tac_list, t'
+      end else begin
+	let tac,f = reduce_factor f1 in
+	let tac',t' = condense t in 
+	[do_both (do_list tac) (do_list tac')], Oplus(f,t') 
+      end
+  | (Oplus(f1,Oz n) as t) -> 
+      let tac,f1' = reduce_factor f1 in 
+      [do_left (do_list tac)],Oplus(f1',Oz n)
+  | Oplus(f1,f2) -> 
+      if weight f1 = weight f2 then begin
+	let tac_shrink,t = shrink_pair f1 f2 in
+	let tac,t' = condense t in
+	tac_shrink :: tac,t'
+      end else begin
+	let tac,f = reduce_factor f1 in
+	let tac',t' = condense f2 in 
+	[do_both (do_list tac) (do_list tac')],Oplus(f,t') 
+      end
+  | (Oz _ as t)-> [],t
+  | t -> 
+      let tac,t' = reduce_factor t in
+      let final = Oplus(t',Oz 0) in
+      tac @ [Lazy.force coq_c_red6], final
+
+(* \subsection{Elimination des zéros} *)
+
+let rec clear_zero = function
+   Oplus(Otimes(Oatom v,Oz 0),r) ->
+     let tac',t = clear_zero r in
+     Lazy.force coq_c_red5 :: tac',t
+  | Oplus(f,r) -> 
+      let tac,t = clear_zero r in 
+      (if tac = [] then [] else [do_right (do_list tac)]),Oplus(f,t)
+  | t -> [],t;;
+
+(* \section{Transformation des hypothèses} *)
+
+let rec reduce = function
+    Oplus(t1,t2) ->
+      let t1', trace1 = reduce t1 in
+      let t2', trace2 = reduce t2 in
+      let trace3,t' = shuffle (t1',t2') in
+      t', do_list [do_both trace1 trace2; trace3]
+  | Ominus(t1,t2) ->
+      let t,trace = reduce (Oplus(t1, Oinv t2)) in
+      t, do_list [Lazy.force coq_c_minus; trace]
+  | Otimes(t1,t2) as t ->
+      let t1', trace1 = reduce t1 in
+      let t2', trace2 = reduce t2 in
+      begin match t1',t2' with
+      | (_, Oz n) ->
+	  let tac,t' = scalar n t1' in
+	  t', do_list [do_both trace1 trace2; tac]
+      | (Oz n,_) ->
+	  let tac,t' = scalar n t2' in
+	  t', do_list [do_both trace1 trace2; Lazy.force coq_c_mult_sym; tac]
+      | _ -> Oufo t, Lazy.force coq_c_nop
+      end
+  | Oinv t ->
+      let t',trace = reduce  t in
+      let trace',t'' = negate t' in
+      t'', do_list [do_left trace; trace']
+  | (Oz _ | Oatom _ | Oufo _) as t -> t, Lazy.force coq_c_nop
+
+let rec ocompile env t =
+  try match destructurate t with
+  | Kapp("Zplus",[t1;t2]) ->
+      let t1',env1 = ocompile env  t1 in
+      let t2',env2 = ocompile env1 t2 in
+      (Oplus (t1',t2'), env2)
+  | Kapp("Zminus",[t1;t2]) ->
+      let t1',env1 = ocompile env  t1 in
+      let t2',env2 = ocompile env1 t2 in
+      (Ominus (t1',t2'), env2)
+  | Kapp("Zmult",[t1;t2]) ->
+      let t1',env1 = ocompile env t1 in
+      let t2',env2 = ocompile env1 t2 in
+      (Otimes (t1',t2'), env2)
+  | Kapp(("POS"|"NEG"|"ZERO"),_) -> 
+      begin try (Oz(recognize_number t),env) 
+      with _ -> 
+	let v,env' = add_atom t env in Oatom v, env'
+      end
+  | Kvar s ->
+      let v,env' = add_atom t env in Oatom v, env'
+  | Kapp("Zopp",[t]) ->
+      let t',env1 = ocompile env t in Oinv t', env1
+  | _ -> 
+      let v,env' = add_atom t env in Oatom(v), env'
+  with e when Logic.catchable_exception e ->
+    let v,env' = add_atom t env in Oatom(v), env'
+
+(*i  | Kapp("Zs",[t1]) ->
+    | Kapp("inject_nat",[t']) -> i*)
+
+let normalize_equation t =
+  let t1,trace1 = reduce t in
+  let trace2,t2 = condense t1 in
+  let trace3,t3 = clear_zero t2 in
+  do_list [trace1; do_list trace2; do_list trace3], t3
+
+let destructure_omega gl (trace_norm, system, env) (id,c) = 
+  let mk_step t1 t2 f kind coq_t_oper =
+       let o1,env1 = ocompile env t1 in
+       let o2,env2 = ocompile env1 t2 in
+       let t = f o1 o2 in
+       let trace, oterm = normalize_equation t in
+       let equa = compile id kind oterm in
+       let tterm =
+	 mkApp (Lazy.force coq_t_oper,
+		[| val_of_formula o1; val_of_formula o2 |]) in
+       ((id,(trace,tterm)) :: trace_norm), (equa :: system), env2 in
+
+  try match destructurate c with
+    | Kapp("eq",[typ;t1;t2]) when destructurate (Tacmach.pf_nf gl typ) = 
+	                          Kapp("Z",[]) ->
+         mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oinv o2)) Omega.EQUA coq_t_equal
+    | Kapp("Zne",[t1;t2]) ->
+        mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oinv o2)) Omega.DISE coq_t_neq
+    | Kapp("Zle",[t1;t2]) ->
+        mk_step t1 t2 (fun o1 o2 -> Oplus (o2,Oinv o1)) Omega.INEQ coq_t_leq
+    | Kapp("Zlt",[t1;t2]) ->
+        mk_step t1 t2 
+	  (fun o1 o2 -> Oplus (Oplus(o2,Oz (-1)),Oinv o1)) Omega.INEQ coq_t_lt
+    | Kapp("Zge",[t1;t2]) ->
+        mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oinv o2)) Omega.INEQ coq_t_geq
+    | Kapp("Zgt",[t1;t2]) ->
+        mk_step t1 t2 
+	  (fun o1 o2 -> Oplus (Oplus(o1,Oz (-1)),Oinv o2)) Omega.INEQ coq_t_gt
+    | _ -> trace_norm, system, env
+  with e when Logic.catchable_exception e -> trace_norm, system, env
+
+(* \section{Rejouer l'historique} *)
+
+let replay_history env_hyp =
+  let rec loop env_hyp t =
+    match t with
+      | Omega.CONTRADICTION (e1,e2) :: l -> 
+	  let trace = mk_nat (List.length e1.Omega.body) in
+	  mkApp (Lazy.force coq_s_contradiction,
+		 [| trace ; mk_nat (get_hyp env_hyp e1.Omega.id); 
+		    mk_nat (get_hyp env_hyp e2.Omega.id) |])
+      | Omega.DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
+	  mkApp (Lazy.force coq_s_div_approx,
+		 [| mk_Z k; mk_Z d; val_of e2.Omega.body e2.Omega.constant;
+		    mk_nat (List.length e2.Omega.body); 
+		    loop env_hyp l; mk_nat (get_hyp env_hyp e1.Omega.id) |])
+      | Omega.NOT_EXACT_DIVIDE (e1,k) :: l ->
+	  let e2_constant = Omega.floor_div e1.Omega.constant k in
+	  let d = e1.Omega.constant - e2_constant * k in
+	  let e2_body = Omega.map_eq_linear (fun c -> c / k) e1.Omega.body in
+          mkApp (Lazy.force coq_s_not_exact_divide,
+		 [|mk_Z k; mk_Z d; val_of e2_body e2_constant; 
+		   mk_nat (List.length e2_body); 
+		   mk_nat (get_hyp env_hyp e1.Omega.id)|])
+      | Omega.EXACT_DIVIDE (e1,k) :: l ->
+	  let e2_body =  Omega.map_eq_linear (fun c -> c / k) e1.Omega.body in
+	  let e2_constant = Omega.floor_div e1.Omega.constant k in
+          mkApp (Lazy.force coq_s_exact_divide,
+		 [|mk_Z k; val_of e2_body e2_constant; 
+		   mk_nat (List.length e2_body);
+		   loop env_hyp l; mk_nat (get_hyp env_hyp e1.Omega.id)|])
+      | (Omega.MERGE_EQ(e3,e1,e2)) :: l ->
+	  let n1 = get_hyp env_hyp e1.Omega.id and n2 = get_hyp env_hyp e2 in
+          mkApp (Lazy.force coq_s_merge_eq,
+		 [| mk_nat (List.length e1.Omega.body);
+		    mk_nat n1; mk_nat n2;
+		    loop (e3:: env_hyp) l |])
+      | Omega.SUM(e3,(k1,e1),(k2,e2)) :: l ->
+	  let n1 = get_hyp env_hyp e1.Omega.id 
+	  and n2 = get_hyp env_hyp e2.Omega.id in
+	  let trace = shuffle_path k1 e1.Omega.body k2 e2.Omega.body in
+          mkApp (Lazy.force coq_s_sum,
+		 [| mk_Z k1; mk_nat n1; mk_Z k2;
+		    mk_nat n2; trace; (loop (e3 :: env_hyp) l) |])
+      | Omega.CONSTANT_NOT_NUL(e,k) :: l -> 
+          mkApp (Lazy.force coq_s_constant_not_nul,
+		 [|  mk_nat (get_hyp env_hyp e) |])
+      | Omega.CONSTANT_NEG(e,k) :: l ->
+          mkApp (Lazy.force coq_s_constant_neg,
+		 [|  mk_nat (get_hyp env_hyp e) |])
+      | Omega.STATE (new_eq,def,orig,m,sigma) :: l ->
+	  let n1 = get_hyp env_hyp orig.Omega.id 
+	  and n2 = get_hyp env_hyp def.Omega.id in
+	  let v = unintern_id sigma in
+	  let o_def = decompile def in
+	  let o_orig = decompile orig in
+	  let body =
+	     Oplus (o_orig,Otimes (Oplus (Oinv v,o_def), Oz m)) in
+	  let trace,_ = normalize_equation body in
+	  mkApp (Lazy.force coq_s_state,
+		 [| mk_Z m; trace; mk_nat n1; mk_nat n2; 
+		    loop (new_eq.Omega.id :: env_hyp) l |])
+      |	Omega.HYP _ :: l -> loop env_hyp l
+      |	Omega.CONSTANT_NUL e :: l ->
+	  mkApp (Lazy.force coq_s_constant_nul, 
+		 [|  mk_nat (get_hyp env_hyp e) |])
+      |	Omega.NEGATE_CONTRADICT(e1,e2,b) :: l ->
+	  mkApp (Lazy.force coq_s_negate_contradict, 
+		 [|  mk_nat (get_hyp env_hyp e1.Omega.id);
+		     mk_nat (get_hyp env_hyp e2.Omega.id) |])
+      | Omega.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
+	  let i =  get_hyp env_hyp e.Omega.id in
+	  let r1 = loop (e1 :: env_hyp) l1 in
+	  let r2 = loop (e2 :: env_hyp) l2 in
+	  mkApp (Lazy.force coq_s_split_ineq, 
+                  [| mk_nat (List.length e.Omega.body); mk_nat i; r1 ; r2 |])
+      |	(Omega.FORGET_C _ | Omega.FORGET _ | Omega.FORGET_I _) :: l ->
+	  loop env_hyp l
+      | (Omega.WEAKEN  _ ) :: l -> failwith "not_treated"
+      |	[] -> failwith "no contradiction"
+  in loop env_hyp
+
+let show_goal gl =
+  if !debug then Pp.pPNL (Tacmach.pr_gls gl); Tacticals.tclIDTAC gl
+
+(* Cette fonction prépare le rejeu puis l'appelle :
+   \begin{itemize}
+   \item elle isole les hypothèses utiles et les mets dans 
+   le but réifié
+   \item elle prépare l'introduction de nouvelles variables pour le test
+    de Banerjee (opération STATE) 
+   \end{itemize}
+*)
+
+let prepare_and_play env tac_hyps trace_solution =   
+  let rec loop ((l_tac_norm, l_terms, l_id, l_e) as result) = function
+    Omega.HYP e :: l ->
+      let id = tag_of_equation e.Omega.id in
+      let (tac_norm,term) = 
+	try List.assoc id tac_hyps
+        with Not_found -> failwith "what eqn" in
+      loop (tac_norm :: l_tac_norm,term :: l_terms,
+	    Term.mkVar id :: l_id, e.Omega.id :: l_e ) l
+  |  Omega.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
+      loop (loop result l1) l2
+  | _ :: l -> loop result l
+  | [] -> result in
+  let l_tac_norms, l_terms,l_generalized, l_e = 
+    loop ([],[],[],[]) trace_solution in
+
+  let rec loop ((env,l_tac_norm, l_terms,l_gener, l_e) as result) = function
+    Omega.STATE (new_eq,def,orig,m,sigma) :: l ->
+      let o_def = decompile def in
+      let coq_def = coq_of_formula env o_def in
+      let v,env' = add_atom coq_def env in
+      intern_id_force (Oatom v) sigma;
+      let term_to_generalize =
+	mkApp(Lazy.force coq_refl_equal,[|Lazy.force coq_Z; coq_def|]) in
+      let reified_term =
+	 mkApp (Lazy.force coq_t_equal,	
+		[| val_of_formula o_def; val_of_formula (Oatom v) |]) in
+      loop (env', Lazy.force coq_c_nop :: l_tac_norm,
+	    reified_term :: l_terms ,term_to_generalize :: l_gener, 
+	    def.Omega.id :: l_e)  l
+  | Omega.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
+      loop (loop result l1) l2
+  | _ :: l -> loop result l
+  | [] -> result in
+  let env, l_tac_norms, l_terms,l_generalized, l_e = 
+    loop (env, l_tac_norms, l_terms,l_generalized, l_e) trace_solution in
+
+  (* Attention Generalize ajoute les buts dans l'ordre inverse *)
+  let l_reified_terms = mk_list (Lazy.force coq_proposition) l_terms in
+  let l_reified_tac_norms = mk_list (Lazy.force coq_step) l_tac_norms in
+  let env_reified = mk_list (Lazy.force coq_Z) env in
+  let reified = 
+    mkApp(Lazy.force coq_interp_sequent, [| env_reified; l_reified_terms |]) in
+  let reified_trace_solution = replay_history l_e trace_solution in
+  if !debug then begin
+    Pp.pPNL [< Printer.prterm reified>];
+    Pp.pPNL [< Printer.prterm l_reified_tac_norms>];
+    Pp.pPNL [< Printer.prterm reified_trace_solution>];
+  end;
+  Tactics.generalize l_generalized >>
+  Tactics.change_in_concl reified >>
+  Tacticals.tclTRY 
+    (Tactics.apply (mkApp (Lazy.force coq_normalize_sequent, 
+			   [|l_reified_tac_norms |]))) >>
+  Tacticals.tclTRY 
+    (Tactics.apply (mkApp (Lazy.force coq_execute_sequent, 
+			   [|reified_trace_solution |]))) >>
+  Tactics.normalise_in_concl >> Auto.auto 5 []
+  
+let coq_omega gl =
+  clear_tags (); clear_intern ();
+  let tactic_hyps, system, env = 
+    List.fold_left (destructure_omega gl) ([],[],[])
+      (Tacmach.pf_hyps_types gl) in
+  if !debug then begin Omega.display_system system;  print_newline () end;
+  begin try
+    let trace = Omega.simplify_strong system in 
+    if !debug then Omega.display_action trace;
+    prepare_and_play env tactic_hyps trace gl
+  with Omega.NO_CONTRADICTION -> Util.error "Omega can't solve this system"
+  end
+
+let refl_omega = Tacmach.hide_atomic_tactic "StepOmega" coq_omega 
+
+(* \section{Encapsulation ROMEGA} *)
+
+(* Toute cette partie est héritée de [OMEGA]. Seule modification : l'appel
+   à [coq_omega] qui correspond à la version réflexive. Il suffirait de 
+   paramétrer le code par cette tactique.
+
+   \paragraph{Note :} cette partie aussi devrait être réfléchie.  *)
+
+open Reduction
+open Proof_type
+open Ast
+open Names
+open Term
+open Environ
+open Sign
+open Inductive
+open Tacmach
+open Tactics
+open Clenv
+open Logic
+open Omega
+
+let nat_inject gl = Coq_omega.nat_inject gl
+let elim_id id gl = simplest_elim (pf_global gl id) gl
+let resolve_id id gl = apply (pf_global gl id) gl
+let generalize_tac = Coq_omega.generalize_tac
+let coq_imp_simp = Coq_omega.coq_imp_simp
+let decidability = Coq_omega.decidability
+let coq_not_or = Coq_omega.coq_not_or
+let coq_not_and = Coq_omega.coq_not_and
+let coq_not_imp = Coq_omega.coq_not_imp
+let coq_not_not = Coq_omega.coq_not_not
+let coq_not_Zle = Coq_omega.coq_not_Zle
+let coq_not_Zge = Coq_omega.coq_not_Zge
+let coq_not_Zlt = Coq_omega.coq_not_Zlt
+let coq_not_Zgt = Coq_omega.coq_not_Zgt
+let coq_not_le = Coq_omega.coq_not_le
+let coq_not_ge = Coq_omega.coq_not_ge
+let coq_not_lt = Coq_omega.coq_not_lt
+let coq_not_gt = Coq_omega.coq_not_gt
+let coq_not_eq = Coq_omega.coq_not_eq
+let coq_not_Zeq = Coq_omega.coq_not_Zeq
+let coq_neq = Coq_omega.coq_neq
+let coq_Zne = Coq_omega.coq_Zne
+let coq_dec_not_not = Coq_omega.coq_dec_not_not
+let old_style_flag = Coq_omega.old_style_flag
+let unfold = Coq_omega.unfold
+let sp_not = Coq_omega.sp_not
+let all_time = Coq_omega.all_time
+let mkNewMeta = Coq_omega.mkNewMeta
+	  
+let destructure_hyps gl =
+  let rec loop evbd = function
+    | [] -> (tclTHEN nat_inject coq_omega)
+    | (i,t)::lit ->
+	begin try match destructurate t with
+          | Kapp(("Zle"|"Zge"|"Zgt"|"Zlt"|"Zne"),[t1;t2]) -> loop evbd lit
+          | Kapp("or",[t1;t2]) ->
+              (tclTHENS ((tclTHEN ((tclTHEN (elim_id i) (clear [i]))) 
+			    (intros_using [i]))) 
+		 ([ loop evbd ((i,t1)::lit); loop evbd ((i,t2)::lit) ]))
+          | Kapp("and",[t1;t2]) ->
+              let i1 = id_of_string (string_of_id i ^ "_left") in
+              let i2 = id_of_string (string_of_id i ^ "_right") in
+              (tclTHEN 
+		 (tclTHEN 
+		    (tclTHEN (elim_id i) (clear [i]))
+		    (intros_using [i1;i2]))
+		 (loop (i1::i2::evbd) ((i1,t1)::(i2,t2)::lit)))
+          | Kimp(t1,t2) ->
+              if isprop (pf_type_of gl t1) & closed0 t2 then begin
+		(tclTHEN 
+		   (tclTHEN 
+		      (tclTHEN
+			 (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| 
+						    t1; t2; 
+						    decidability gl t1;
+						    mkVar i|])]) 
+			 (clear [i])) 
+		      (intros_using [i])) 
+		   (loop evbd ((i,mk_or (mk_not t1) t2)::lit)))
+              end else loop evbd lit
+          | Kapp("not",[t]) -> 
+              begin match destructurate t with 
+		  Kapp("or",[t1;t2]) -> 
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN 
+			     (generalize_tac [mkApp (Lazy.force coq_not_or,[| 
+							t1; t2; mkVar i |])])
+			     (clear [i])) 
+			  (intros_using [i])) 
+                       (loop evbd ((i,mk_and (mk_not t1) (mk_not t2)):: lit)))
+		| Kapp("and",[t1;t2]) -> 
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN
+			     (generalize_tac
+				[mkApp (Lazy.force coq_not_and, [| t1; t2;
+					   decidability gl t1;mkVar i|])])
+			     (clear [i]))
+			  (intros_using [i]))
+                       (loop evbd ((i,mk_or (mk_not t1) (mk_not t2))::lit)))
+		| Kimp(t1,t2) ->
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN
+			     (generalize_tac 
+				[mkApp (Lazy.force coq_not_imp, [| t1; t2; 
+					   decidability gl t1;mkVar i |])])
+			     (clear [i])) 
+			  (intros_using [i]))
+                       (loop evbd ((i,mk_and t1 (mk_not t2)) :: lit)))
+		| Kapp("not",[t]) ->
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN
+			     (generalize_tac
+				[mkApp (Lazy.force coq_not_not, [| t;
+					    decidability gl t; mkVar i |])])
+			     (clear [i])) 
+			  (intros_using [i])) 
+                       (loop evbd ((i,t)::lit)))
+		| Kapp("Zle", [t1;t2]) ->
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN
+			     (generalize_tac [mkApp (Lazy.force coq_not_Zle,
+							[| t1;t2;mkVar i|])])
+			     (clear [i])) 
+			  (intros_using [i])) 
+		       (loop evbd lit))
+		| Kapp("Zge", [t1;t2]) ->
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN
+			     (generalize_tac [mkApp (Lazy.force coq_not_Zge,
+							[| t1;t2;mkVar i|])])
+			     (clear [i])) 
+			  (intros_using [i])) 
+		       (loop evbd lit))
+		| Kapp("Zlt", [t1;t2]) ->
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN
+			     (generalize_tac [mkApp (Lazy.force coq_not_Zlt,
+							[| t1;t2;mkVar i|])])
+			     (clear [i])) 
+			  (intros_using [i])) 
+		       (loop evbd lit))
+		| Kapp("Zgt", [t1;t2]) ->
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN
+			     (generalize_tac [mkApp (Lazy.force coq_not_Zgt,
+							[| t1;t2;mkVar i|])])
+			     (clear [i])) 
+			  (intros_using [i])) 
+		       (loop evbd lit))
+		| Kapp("le", [t1;t2]) ->
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN
+			     (generalize_tac [mkApp (Lazy.force coq_not_le,
+							[| t1;t2;mkVar i|])])
+			     (clear [i])) 
+			  (intros_using [i])) 
+		       (loop evbd lit))
+		| Kapp("ge", [t1;t2]) ->
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN
+			     (generalize_tac [mkApp (Lazy.force coq_not_ge,
+							[| t1;t2;mkVar i|])])
+			     (clear [i])) 
+			  (intros_using [i])) 
+		       (loop evbd lit))
+		| Kapp("lt", [t1;t2]) ->
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN
+			     (generalize_tac [mkApp (Lazy.force coq_not_lt,
+							[| t1;t2;mkVar i|])])
+			     (clear [i])) 
+			  (intros_using [i])) 
+		       (loop evbd lit))
+		| Kapp("gt", [t1;t2]) ->
+                    (tclTHEN 
+		       (tclTHEN 
+			  (tclTHEN
+			     (generalize_tac [mkApp (Lazy.force coq_not_gt,
+							[| t1;t2;mkVar i|])])
+			     (clear [i])) 
+			  (intros_using [i])) 
+		       (loop evbd lit))
+		| Kapp("eq",[typ;t1;t2]) ->
+                    if !old_style_flag then begin 
+		      match destructurate (pf_nf gl typ) with
+			| Kapp("nat",_) -> 
+                            (tclTHEN 
+			       (tclTHEN 
+				  (tclTHEN 
+				     (simplest_elim 
+					(applist 
+					   (Lazy.force coq_not_eq, 
+					    [t1;t2;mkVar i])))
+				     (clear [i])) 
+				  (intros_using [i])) 
+			       (loop evbd lit))
+			| Kapp("Z",_) ->
+                            (tclTHEN 
+			       (tclTHEN 
+				  (tclTHEN 
+				     (simplest_elim 
+					(applist 
+					   (Lazy.force coq_not_Zeq, 
+					    [t1;t2;mkVar i])))
+				     (clear [i])) 
+				  (intros_using [i])) 
+			       (loop evbd lit))
+			| _ -> loop evbd lit
+                    end else begin 
+		      match destructurate (pf_nf gl typ) with
+			| Kapp("nat",_) -> 
+                            (tclTHEN 
+			       (convert_hyp i 
+				  (mkApp (Lazy.force coq_neq, [| t1;t2|])))
+			       (loop evbd lit))
+			| Kapp("Z",_) ->
+                            (tclTHEN 
+			       (convert_hyp i 
+				  (mkApp (Lazy.force coq_Zne, [| t1;t2|])))
+			       (loop evbd lit))
+			| _ -> loop evbd lit
+                    end
+		| _ -> loop evbd lit
+              end 
+          | _ -> loop evbd lit 
+	with e when catchable_exception e -> loop evbd lit
+	end 
+  in
+  loop (pf_ids_of_hyps gl) (pf_hyps_types gl) gl
+
+let omega_solver gl =
+  let concl = pf_concl gl in
+  let rec loop t =
+    match destructurate t with
+      | Kapp("not",[t1;t2]) -> 
+          (tclTHEN 
+	     (tclTHEN (unfold sp_not) intro) 
+	     destructure_hyps)
+      | Kimp(a,b) -> (tclTHEN intro (loop b))
+      | Kapp("False",[]) -> destructure_hyps
+      | _ ->
+          (tclTHEN 
+	     (tclTHEN
+		(Tactics.refine 
+		   (mkApp (Lazy.force coq_dec_not_not, [| t;
+			      decidability gl t; mkNewMeta () |])))
+		intro) 
+	     (destructure_hyps)) 
+  in
+  (loop concl) gl
+
+let omega = hide_atomic_tactic "ReflOmega" omega_solver
diff --git a/kernel/names.ml b/kernel/names.ml
index 6633ba238..a6463a7bd 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -113,7 +113,8 @@ let check_ident s =
   let l = String.length s in
   if l = 0 then error "The empty string is not an identifier";
   let c = String.get s 0 in
-  if (is_letter c) or c = '_' or c = '$' then check_ident_suffix 1 l s
+  if (is_letter c) or c = '_' or c = '$' or c = '?' 
+  then check_ident_suffix 1 l s
   else error (s^": an identifier should start with a letter")
 
 let is_ident s = try check_ident s; true with _ -> false