From 2bb2d480b547e58deb2ec62791c8990ecac777b0 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 10 Apr 2001 13:21:45 +0000
Subject: réparation Correctness; options Extraction (changement de syntaxe)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 .depend                                | 424 ++++++++++++++++++++++++++++++++-
 .depend.camlp4                         |   2 +-
 Makefile                               |   7 +-
 contrib/correctness/Correctness.v      |   9 -
 contrib/correctness/examples/exp.v     |  13 +-
 contrib/correctness/examples/exp_int.v |   8 +-
 contrib/correctness/pcic.ml            |   5 +-
 contrib/correctness/pmisc.ml           |   8 +-
 contrib/correctness/pmisc.mli          |   6 +-
 contrib/correctness/pmonad.ml          |  24 +-
 contrib/correctness/psyntax.ml4        |   2 +-
 contrib/correctness/ptactic.ml         |  22 +-
 contrib/extraction/Extraction.v        |   8 +-
 contrib/extraction/extract_env.ml      |   6 +-
 contrib/extraction/mlutil.ml           |  24 +-
 contrib/extraction/mlutil.mli          |   2 +-
 kernel/reduction.ml                    |  12 +-
 17 files changed, 493 insertions(+), 89 deletions(-)

diff --git a/.depend b/.depend
index d368b2372d..1bc5ebc1b8 100644
--- a/.depend
+++ b/.depend
@@ -207,12 +207,68 @@ toplevel/vernacentries.cmi: parsing/coqast.cmi kernel/environ.cmi \
     kernel/term.cmi toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     library/nametab.cmi proofs/proof_type.cmi 
+contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \
+    contrib/correctness/ptype.cmi kernel/term.cmi 
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+    pretyping/rawterm.cmi 
+contrib/correctness/pcicenv.cmi: kernel/names.cmi \
+    contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
+    kernel/sign.cmi kernel/term.cmi 
+contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
+    contrib/correctness/ptype.cmi 
+contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi 
+contrib/correctness/penv.cmi: kernel/names.cmi contrib/correctness/past.cmi \
+    contrib/correctness/ptype.cmi kernel/term.cmi 
+contrib/correctness/perror.cmi: parsing/coqast.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi contrib/correctness/peffect.cmi lib/pp.cmi \
+    contrib/correctness/ptype.cmi 
+contrib/correctness/pextract.cmi: kernel/names.cmi 
+contrib/correctness/pmisc.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/term.cmi 
+contrib/correctness/pmlize.cmi: kernel/names.cmi contrib/correctness/past.cmi \
+    contrib/correctness/penv.cmi contrib/correctness/prename.cmi 
+contrib/correctness/pmonad.cmi: kernel/names.cmi contrib/correctness/past.cmi \
+    contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    kernel/term.cmi 
+contrib/correctness/pred.cmi: contrib/correctness/past.cmi kernel/term.cmi 
+contrib/correctness/prename.cmi: kernel/names.cmi lib/pp.cmi 
+contrib/correctness/psyntax.cmi: parsing/coqast.cmi \
+    contrib/correctness/past.cmi parsing/pcoq.cmi \
+    contrib/correctness/ptype.cmi 
+contrib/correctness/ptactic.cmi: contrib/correctness/past.cmi \
+    proofs/tacmach.cmi 
+contrib/correctness/ptype.cmi: kernel/names.cmi \
+    contrib/correctness/peffect.cmi kernel/term.cmi 
+contrib/correctness/ptyping.cmi: parsing/coqast.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    kernel/term.cmi 
+contrib/correctness/putil.cmi: kernel/names.cmi contrib/correctness/past.cmi \
+    contrib/correctness/penv.cmi contrib/correctness/pmisc.cmi lib/pp.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    kernel/term.cmi 
+contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \
+    contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
+    kernel/term.cmi 
 contrib/extraction/extraction.cmi: kernel/environ.cmi \
     contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi 
 contrib/extraction/miniml.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 contrib/extraction/mlutil.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
     kernel/term.cmi 
-contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi 
+contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi \
+    contrib/extraction/mlutil.cmi 
+contrib/interface/dad.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
+    proofs/tacmach.cmi 
+contrib/interface/debug_tac.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
+    proofs/tacmach.cmi 
+contrib/interface/name_to_ast.cmi: parsing/coqast.cmi library/nametab.cmi 
+contrib/interface/pbp.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
+    proofs/tacmach.cmi 
+contrib/interface/translate.cmi: contrib/interface/ascent.cmi \
+    kernel/environ.cmi kernel/evd.cmi proofs/proof_type.cmi kernel/term.cmi 
+contrib/interface/vtp.cmi: contrib/interface/ascent.cmi 
+contrib/interface/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 
@@ -1288,6 +1344,232 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
     proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \
     toplevel/vernacinterp.cmi 
+contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \
+    library/declare.cmi pretyping/detyping.cmi kernel/names.cmi \
+    library/nametab.cmi contrib/correctness/past.cmi \
+    contrib/correctness/pmisc.cmi pretyping/rawterm.cmi toplevel/record.cmi \
+    kernel/sign.cmi kernel/term.cmi lib/util.cmi contrib/correctness/pcic.cmi 
+contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \
+    library/declare.cmx pretyping/detyping.cmx kernel/names.cmx \
+    library/nametab.cmx contrib/correctness/past.cmi \
+    contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \
+    kernel/sign.cmx kernel/term.cmx lib/util.cmx contrib/correctness/pcic.cmi 
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
+contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \
+    kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
+    contrib/correctness/penv.cmi contrib/correctness/perror.cmi \
+    contrib/correctness/ptype.cmi kernel/sign.cmi kernel/term.cmi \
+    contrib/correctness/pdb.cmi 
+contrib/correctness/pdb.cmx: library/declare.cmx library/global.cmx \
+    kernel/names.cmx library/nametab.cmx contrib/correctness/past.cmi \
+    contrib/correctness/penv.cmx contrib/correctness/perror.cmx \
+    contrib/correctness/ptype.cmi kernel/sign.cmx kernel/term.cmx \
+    contrib/correctness/pdb.cmi 
+contrib/correctness/peffect.cmo: toplevel/himsg.cmi kernel/names.cmi \
+    contrib/correctness/pmisc.cmi lib/pp.cmi lib/util.cmi \
+    contrib/correctness/peffect.cmi 
+contrib/correctness/peffect.cmx: toplevel/himsg.cmx kernel/names.cmx \
+    contrib/correctness/pmisc.cmx lib/pp.cmx lib/util.cmx \
+    contrib/correctness/peffect.cmi 
+contrib/correctness/penv.cmo: toplevel/himsg.cmi library/lib.cmi \
+    library/libobject.cmi library/library.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi contrib/correctness/perror.cmi \
+    contrib/correctness/pmisc.cmi lib/pp.cmi contrib/correctness/ptype.cmi \
+    library/summary.cmi kernel/term.cmi contrib/correctness/penv.cmi 
+contrib/correctness/penv.cmx: toplevel/himsg.cmx library/lib.cmx \
+    library/libobject.cmx library/library.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi contrib/correctness/perror.cmx \
+    contrib/correctness/pmisc.cmx lib/pp.cmx contrib/correctness/ptype.cmi \
+    library/summary.cmx kernel/term.cmx contrib/correctness/penv.cmi 
+contrib/correctness/perror.cmo: library/declare.cmi kernel/evd.cmi \
+    library/global.cmi toplevel/himsg.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi contrib/correctness/peffect.cmi lib/pp.cmi \
+    contrib/correctness/ptype.cmi kernel/reduction.cmi kernel/term.cmi \
+    lib/util.cmi contrib/correctness/perror.cmi 
+contrib/correctness/perror.cmx: library/declare.cmx kernel/evd.cmx \
+    library/global.cmx toplevel/himsg.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi contrib/correctness/peffect.cmx lib/pp.cmx \
+    contrib/correctness/ptype.cmi kernel/reduction.cmx kernel/term.cmx \
+    lib/util.cmx contrib/correctness/perror.cmi 
+contrib/correctness/pextract.cmo: parsing/ast.cmi kernel/evd.cmi \
+    toplevel/himsg.cmi library/library.cmi kernel/names.cmi \
+    library/nametab.cmi contrib/extraction/ocaml.cmi \
+    contrib/correctness/past.cmi contrib/correctness/pcicenv.cmi \
+    contrib/correctness/penv.cmi lib/pp.cmi lib/pp_control.cmi \
+    contrib/correctness/ptype.cmi contrib/correctness/putil.cmi \
+    kernel/reduction.cmi lib/system.cmi kernel/term.cmi lib/util.cmi \
+    toplevel/vernacinterp.cmi contrib/correctness/pextract.cmi 
+contrib/correctness/pextract.cmx: parsing/ast.cmx kernel/evd.cmx \
+    toplevel/himsg.cmx library/library.cmx kernel/names.cmx \
+    library/nametab.cmx contrib/extraction/ocaml.cmx \
+    contrib/correctness/past.cmi contrib/correctness/pcicenv.cmx \
+    contrib/correctness/penv.cmx lib/pp.cmx lib/pp_control.cmx \
+    contrib/correctness/ptype.cmi contrib/correctness/putil.cmx \
+    kernel/reduction.cmx lib/system.cmx kernel/term.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmx contrib/correctness/pextract.cmi 
+contrib/correctness/pmisc.cmo: parsing/coqast.cmi library/declare.cmi \
+    pretyping/evarutil.cmi library/global.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/term.cmi lib/util.cmi contrib/correctness/pmisc.cmi 
+contrib/correctness/pmisc.cmx: parsing/coqast.cmx library/declare.cmx \
+    pretyping/evarutil.cmx library/global.cmx kernel/names.cmx lib/pp.cmx \
+    kernel/term.cmx lib/util.cmx contrib/correctness/pmisc.cmi 
+contrib/correctness/pmlize.cmo: parsing/coqlib.cmi kernel/evd.cmi \
+    library/global.cmi kernel/names.cmi contrib/correctness/past.cmi \
+    pretyping/pattern.cmi contrib/correctness/pcicenv.cmi \
+    contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    contrib/correctness/ptyping.cmi contrib/correctness/putil.cmi \
+    kernel/term.cmi parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \
+    contrib/correctness/pmlize.cmi 
+contrib/correctness/pmlize.cmx: parsing/coqlib.cmx kernel/evd.cmx \
+    library/global.cmx kernel/names.cmx contrib/correctness/past.cmi \
+    pretyping/pattern.cmx contrib/correctness/pcicenv.cmx \
+    contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+    contrib/correctness/ptyping.cmx contrib/correctness/putil.cmx \
+    kernel/term.cmx parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \
+    contrib/correctness/pmlize.cmi 
+contrib/correctness/pmonad.cmo: kernel/names.cmi contrib/correctness/past.cmi \
+    contrib/correctness/pcic.cmi contrib/correctness/peffect.cmi \
+    contrib/correctness/penv.cmi contrib/correctness/pmisc.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmi kernel/term.cmi parsing/termast.cmi \
+    lib/util.cmi contrib/correctness/pmonad.cmi 
+contrib/correctness/pmonad.cmx: kernel/names.cmx contrib/correctness/past.cmi \
+    contrib/correctness/pcic.cmx contrib/correctness/peffect.cmx \
+    contrib/correctness/penv.cmx contrib/correctness/pmisc.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmx kernel/term.cmx parsing/termast.cmx \
+    lib/util.cmx contrib/correctness/pmonad.cmi 
+contrib/correctness/pred.cmo: kernel/evd.cmi library/global.cmi \
+    contrib/correctness/past.cmi lib/pp.cmi kernel/reduction.cmi \
+    kernel/term.cmi contrib/correctness/pred.cmi 
+contrib/correctness/pred.cmx: kernel/evd.cmx library/global.cmx \
+    contrib/correctness/past.cmi lib/pp.cmx kernel/reduction.cmx \
+    kernel/term.cmx contrib/correctness/pred.cmi 
+contrib/correctness/prename.cmo: toplevel/himsg.cmi kernel/names.cmi \
+    contrib/correctness/pmisc.cmi lib/pp.cmi lib/util.cmi \
+    contrib/correctness/prename.cmi 
+contrib/correctness/prename.cmx: toplevel/himsg.cmx kernel/names.cmx \
+    contrib/correctness/pmisc.cmx lib/pp.cmx lib/util.cmx \
+    contrib/correctness/prename.cmi 
+contrib/correctness/psyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
+    parsing/coqast.cmi library/declare.cmi lib/dyn.cmi kernel/evd.cmi \
+    parsing/g_zsyntax.cmi library/global.cmi toplevel/himsg.cmi \
+    kernel/names.cmi contrib/correctness/past.cmi parsing/pcoq.cmi \
+    contrib/correctness/pdb.cmi contrib/correctness/peffect.cmi \
+    contrib/correctness/penv.cmi contrib/correctness/pmisc.cmi \
+    contrib/correctness/pmonad.cmi lib/pp.cmi contrib/correctness/prename.cmi \
+    contrib/correctness/ptactic.cmi contrib/correctness/ptype.cmi \
+    contrib/correctness/ptyping.cmi contrib/correctness/putil.cmi \
+    kernel/reduction.cmi proofs/tacinterp.cmi kernel/term.cmi \
+    parsing/termast.cmi lib/util.cmi toplevel/vernac.cmi \
+    toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \
+    contrib/correctness/psyntax.cmi 
+contrib/correctness/psyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
+    parsing/coqast.cmx library/declare.cmx lib/dyn.cmx kernel/evd.cmx \
+    parsing/g_zsyntax.cmx library/global.cmx toplevel/himsg.cmx \
+    kernel/names.cmx contrib/correctness/past.cmi parsing/pcoq.cmx \
+    contrib/correctness/pdb.cmx contrib/correctness/peffect.cmx \
+    contrib/correctness/penv.cmx contrib/correctness/pmisc.cmx \
+    contrib/correctness/pmonad.cmx lib/pp.cmx contrib/correctness/prename.cmx \
+    contrib/correctness/ptactic.cmx contrib/correctness/ptype.cmi \
+    contrib/correctness/ptyping.cmx contrib/correctness/putil.cmx \
+    kernel/reduction.cmx proofs/tacinterp.cmx kernel/term.cmx \
+    parsing/termast.cmx lib/util.cmx toplevel/vernac.cmx \
+    toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \
+    contrib/correctness/psyntax.cmi 
+contrib/correctness/ptactic.cmo: toplevel/command.cmi library/declare.cmi \
+    tactics/equality.cmi kernel/evd.cmi library/global.cmi kernel/names.cmi \
+    lib/options.cmi contrib/correctness/past.cmi pretyping/pattern.cmi \
+    contrib/correctness/pcic.cmi contrib/correctness/pdb.cmi \
+    contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/perror.cmi proofs/pfedit.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmlize.cmi \
+    contrib/correctness/pmonad.cmi lib/pp.cmi contrib/correctness/pred.cmi \
+    contrib/correctness/prename.cmi pretyping/pretyping.cmi \
+    parsing/printer.cmi contrib/correctness/ptyping.cmi \
+    contrib/correctness/putil.cmi contrib/correctness/pwp.cmi \
+    kernel/reduction.cmi tactics/refine.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
+    toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \
+    contrib/correctness/ptactic.cmi 
+contrib/correctness/ptactic.cmx: toplevel/command.cmx library/declare.cmx \
+    tactics/equality.cmx kernel/evd.cmx library/global.cmx kernel/names.cmx \
+    lib/options.cmx contrib/correctness/past.cmi pretyping/pattern.cmx \
+    contrib/correctness/pcic.cmx contrib/correctness/pdb.cmx \
+    contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
+    contrib/correctness/perror.cmx proofs/pfedit.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmlize.cmx \
+    contrib/correctness/pmonad.cmx lib/pp.cmx contrib/correctness/pred.cmx \
+    contrib/correctness/prename.cmx pretyping/pretyping.cmx \
+    parsing/printer.cmx contrib/correctness/ptyping.cmx \
+    contrib/correctness/putil.cmx contrib/correctness/pwp.cmx \
+    kernel/reduction.cmx tactics/refine.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
+    toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \
+    contrib/correctness/ptactic.cmi 
+contrib/correctness/ptyping.cmo: parsing/ast.cmi parsing/astterm.cmi \
+    kernel/environ.cmi kernel/evd.cmi library/global.cmi toplevel/himsg.cmi \
+    kernel/names.cmi contrib/correctness/past.cmi \
+    contrib/correctness/pcicenv.cmi contrib/correctness/peffect.cmi \
+    contrib/correctness/penv.cmi contrib/correctness/perror.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi lib/pp.cmi \
+    contrib/correctness/prename.cmi proofs/proof_trees.cmi \
+    contrib/correctness/ptype.cmi contrib/correctness/putil.cmi \
+    kernel/reduction.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
+    contrib/correctness/ptyping.cmi 
+contrib/correctness/ptyping.cmx: parsing/ast.cmx parsing/astterm.cmx \
+    kernel/environ.cmx kernel/evd.cmx library/global.cmx toplevel/himsg.cmx \
+    kernel/names.cmx contrib/correctness/past.cmi \
+    contrib/correctness/pcicenv.cmx contrib/correctness/peffect.cmx \
+    contrib/correctness/penv.cmx contrib/correctness/perror.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx lib/pp.cmx \
+    contrib/correctness/prename.cmx proofs/proof_trees.cmx \
+    contrib/correctness/ptype.cmi contrib/correctness/putil.cmx \
+    kernel/reduction.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
+    contrib/correctness/ptyping.cmi 
+contrib/correctness/putil.cmo: parsing/coqlib.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi pretyping/pattern.cmi \
+    contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi lib/pp.cmi contrib/correctness/prename.cmi \
+    parsing/printer.cmi contrib/correctness/ptype.cmi kernel/term.cmi \
+    lib/util.cmi contrib/correctness/putil.cmi 
+contrib/correctness/putil.cmx: parsing/coqlib.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi pretyping/pattern.cmx \
+    contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx lib/pp.cmx contrib/correctness/prename.cmx \
+    parsing/printer.cmx contrib/correctness/ptype.cmi kernel/term.cmx \
+    lib/util.cmx contrib/correctness/putil.cmi 
+contrib/correctness/pwp.cmo: kernel/evd.cmi library/global.cmi \
+    kernel/names.cmi contrib/correctness/past.cmi \
+    contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/perror.cmi contrib/correctness/pmisc.cmi \
+    contrib/correctness/pmonad.cmi contrib/correctness/prename.cmi \
+    contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmi \
+    contrib/correctness/putil.cmi kernel/reduction.cmi kernel/term.cmi \
+    lib/util.cmi contrib/correctness/pwp.cmi 
+contrib/correctness/pwp.cmx: kernel/evd.cmx library/global.cmx \
+    kernel/names.cmx contrib/correctness/past.cmi \
+    contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
+    contrib/correctness/perror.cmx contrib/correctness/pmisc.cmx \
+    contrib/correctness/pmonad.cmx contrib/correctness/prename.cmx \
+    contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmx \
+    contrib/correctness/putil.cmx kernel/reduction.cmx kernel/term.cmx \
+    lib/util.cmx contrib/correctness/pwp.cmi 
 contrib/extraction/extract_env.cmo: parsing/astterm.cmi kernel/evd.cmi \
     contrib/extraction/extraction.cmi library/global.cmi library/lib.cmi \
     library/libobject.cmi library/library.cmi contrib/extraction/miniml.cmi \
@@ -1332,6 +1614,144 @@ contrib/extraction/ocaml.cmx: kernel/environ.cmx library/global.cmx \
     contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
     kernel/names.cmx lib/pp.cmx lib/pp_control.cmx kernel/term.cmx \
     lib/util.cmx contrib/extraction/ocaml.cmi 
+contrib/interface/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 \
+    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/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 \
+    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/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/dad.cmi 
+contrib/interface/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/dad.cmi 
+contrib/interface/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/debug_tac.cmi 
+contrib/interface/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/debug_tac.cmi 
+contrib/interface/history.cmo: contrib/interface/paths.cmi \
+    contrib/interface/history.cmi 
+contrib/interface/history.cmx: contrib/interface/paths.cmx \
+    contrib/interface/history.cmi 
+contrib/interface/line_parser.cmo: contrib/interface/line_parser.cmi 
+contrib/interface/line_parser.cmx: contrib/interface/line_parser.cmi 
+contrib/interface/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/pretty.cmi \
+    kernel/reduction.cmi kernel/sign.cmi pretyping/syntax_def.cmi \
+    kernel/term.cmi parsing/termast.cmi lib/util.cmi \
+    contrib/interface/name_to_ast.cmi 
+contrib/interface/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/pretty.cmx \
+    kernel/reduction.cmx kernel/sign.cmx pretyping/syntax_def.cmx \
+    kernel/term.cmx parsing/termast.cmx lib/util.cmx \
+    contrib/interface/name_to_ast.cmi 
+contrib/interface/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/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/paths.cmo: contrib/interface/paths.cmi 
+contrib/interface/paths.cmx: contrib/interface/paths.cmi 
+contrib/interface/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/pbp.cmi 
+contrib/interface/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/pbp.cmi 
+contrib/interface/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/translate.cmi 
+contrib/interface/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/translate.cmi 
+contrib/interface/vtp.cmo: contrib/interface/ascent.cmi \
+    contrib/interface/vtp.cmi 
+contrib/interface/vtp.cmx: contrib/interface/ascent.cmi \
+    contrib/interface/vtp.cmi 
+contrib/interface/xlate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
+    parsing/coqast.cmi kernel/names.cmi lib/util.cmi \
+    contrib/interface/xlate.cmi 
+contrib/interface/xlate.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \
+    parsing/coqast.cmx kernel/names.cmx lib/util.cmx \
+    contrib/interface/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 \
@@ -1401,7 +1821,7 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \
 contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/xml/xmlcommand.cmx 
 tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
-contrib/correctness/psyntax.cmo: 
+contrib/correctness/psyntax.cmo: parsing/grammar.cma
 parsing/lexer.cmo: 
 parsing/q_coqast.cmo: 
 parsing/g_prim.cmo: 
diff --git a/.depend.camlp4 b/.depend.camlp4
index 41388d2393..5fa3abb6a0 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -1,5 +1,5 @@
 tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
-contrib/correctness/psyntax.ml: 
+contrib/correctness/psyntax.ml: parsing/grammar.cma
 parsing/lexer.ml: 
 parsing/q_coqast.ml: 
 parsing/g_prim.ml: 
diff --git a/Makefile b/Makefile
index 5d6d667f33..c64d92c39f 100644
--- a/Makefile
+++ b/Makefile
@@ -201,7 +201,7 @@ CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
         contrib/ring/quote.cmo contrib/ring/ring.cmo \
 	contrib/xml/xml.cmo \
 	contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo \
-	$(EXTRACTIONCMO)
+	$(EXTRACTIONCMO) $(CORRECTNESSCMO)
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
@@ -447,9 +447,6 @@ CORRECTNESSVO=contrib/correctness/Arrays.vo				\
 	contrib/correctness/Tuples.vo
 #	contrib/correctness/ProgramsExtraction.vo			
 
-contrib/correctness/%.vo: contrib/correctness/%.v
-	$(COQC) -q -byte -bindir bin $(COQINCLUDES) $<
-
 OMEGAVO = contrib/omega/Omega.vo       contrib/omega/Zlogarithm.vo \
           contrib/omega/OmegaSyntax.vo contrib/omega/Zpower.vo \
           contrib/omega/Zcomplements.vo
@@ -468,7 +465,7 @@ contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE)
 contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE)
 	$(COQC) -q -byte -bindir bin $(COQINCLUDES) $<
 
-CONTRIBVO = $(OMEGAVO) $(RINGVO) $(XMLVO)
+CONTRIBVO = $(OMEGAVO) $(RINGVO) $(XMLVO) $(CORRECTNESSVO)
 
 $(CONTRIBVO): states/initial.coq
 
diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v
index bc12ec7552..0c47512ed7 100644
--- a/contrib/correctness/Correctness.v
+++ b/contrib/correctness/Correctness.v
@@ -22,13 +22,4 @@ Require Export ProgWf.
 
 Require Export Arrays.
 
-Declare ML Module
-    "pmisc" "peffect" "prename" 
-    "perror" "penv" "putil" "pdb" "pcic" "pmonad" "pcicenv"
-    "pred" "ptyping" "pwp" "pmlize" "ptactic" "psyntax".
-
 Token "'".
-
-
-
-
diff --git a/contrib/correctness/examples/exp.v b/contrib/correctness/examples/exp.v
index 1b6bc0b38f..e4aaa49c2c 100644
--- a/contrib/correctness/examples/exp.v
+++ b/contrib/correctness/examples/exp.v
@@ -149,7 +149,7 @@ Correctness i_exp
     let e = ref n in
     begin
       while (notzerop_bool !e) do
-        { invariant (power x n)=(mult y (power m e)) as I
+        { invariant (power x n)=(mult y (power m e)) as Inv
           variant e for lt }
         (if not (even_odd_bool !e) then y := (mult !y !m))
           { (power x n) = (mult y (power m (double (div2 e)))) as Q };
@@ -161,11 +161,10 @@ Correctness i_exp
     { result=(power x n) }
 .
 Proof.
-Rewrite (odd_double e0 Test1) in I. Rewrite I. Simpl. Auto with arith.
+stop.
+Rewrite (odd_double e0 Test1) in Inv. Rewrite Inv. Simpl. Auto with arith.
 
-Rewrite (even_double e0 Test1) in I. Rewrite I. Reflexivity.
-
-Split.
+Rewrite (even_double e0 Test1) in Inv. Rewrite Inv. Reflexivity.
 
 Exact (lt_div2 e0 Test2).
 
@@ -177,8 +176,8 @@ Rewrite (power_2n m0 (div2 e0)). Reflexivity.
 
 Auto with arith.
 
-Decompose [and] I.
-Rewrite H0. Rewrite H1.
+Decompose [and] Inv.
+Rewrite H. Rewrite H0.
 Auto with arith.
 Save.
 
diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v
index dc55eafa13..e6beecccf8 100644
--- a/contrib/correctness/examples/exp_int.v
+++ b/contrib/correctness/examples/exp_int.v
@@ -27,7 +27,7 @@
 Require Zpower.
 Require Zcomplements.
 
-Require Programs.
+Require Correctness.
 Require ZArithRing.
 Require Omega.
 
@@ -52,12 +52,12 @@ Intro. Absurd `0 > 0`; [ Omega | Assumption ].
 Destruct p; Auto with zarith.
 
 Simpl.
-Intro p.
+Intro p0.
 Replace (POS (xI p0)) with `2*(POS p0)+1`.
 Omega.
 Simpl. Auto with zarith.
 
-Intro p.
+Intro p0.
 Simpl.
 Replace (POS (xO p0)) with `2*(POS p0)`.
 Omega.
@@ -120,7 +120,7 @@ Correctness i_exp
     let e = ref n in
     begin
       while !e > 0 do
-        { invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as I
+        { invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as Inv
           variant e }
         (if not (Zeven_odd_bool !e) then y := (Zmult !y !m))
           { (Zpower x n) = (Zmult y (Zpower m (Zdouble (Zdiv2 e)))) as Q };
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index cf233a9889..4395aa53a5 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -185,10 +185,11 @@ let rawconstr_of_prog p =
       	let args = tyl @ cl in
 	RApp (dummy_loc, RRef (dummy_loc, tuple), args)
 
-    | CC_case (_,b,el) ->
+    | CC_case (ty,b,el) ->
 	let c = trad avoid nenv b in
 	let cl = List.map (trad avoid nenv) el in
-	ROldCase (dummy_loc, false, None, c, Array.of_list cl)
+	let ty = Detyping.detype avoid nenv ty in
+	ROldCase (dummy_loc, false, Some ty, c, Array.of_list cl)
 
     | CC_expr c -> 
 	Detyping.detype avoid nenv c
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 77356e17cd..d6a15959b2 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -17,8 +17,6 @@ open Term
 
 module SpSet = Set.Make(struct type t = section_path let compare = sp_ord end)
 
-let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
-
 (* debug *)
 
 let debug = ref false
@@ -148,6 +146,12 @@ let real_subst_in_constr = replace_vars
 
 (* Coq constants *)
 
+let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
+
+let bool_sp = coq_constant ["Init"; "Datatypes"] "bool"
+let coq_true = mkMutConstruct (((bool_sp,0),1), [||])
+let coq_false = mkMutConstruct (((bool_sp,0),2), [||])
+
 let constant s =
   let id = id_of_string s in
   Declare.global_reference CCI id
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index 96519ee9f2..a4359b6d89 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -15,8 +15,6 @@ open Term
 
 module SpSet : Set.S with type elt = section_path
 
-val coq_constant : string list -> string -> section_path
-
 (* Some misc. functions *)
 
 val reraise_with_loc : Coqast.loc -> ('a -> 'b) -> 'a -> 'b
@@ -57,8 +55,12 @@ val subst_ast_in_ast : (identifier * Coqast.t) list -> Coqast.t -> Coqast.t
 val real_subst_in_constr : (identifier * constr) list -> constr -> constr
 
 val constant : string -> constr
+val coq_constant : string list -> string -> section_path
 val conj : constr -> constr -> constr
 
+val coq_true : constr
+val coq_false : constr
+
 val connective_and : identifier
 val connective_or  : identifier
 val connective_not : identifier
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml
index 9d69ecdcbf..49d8d9bf78 100644
--- a/contrib/correctness/pmonad.ml
+++ b/contrib/correctness/pmonad.ml
@@ -402,14 +402,19 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c =
  *)
 
 let make_if_case ren env ty (b,qb) (br1,br2) =
-  let ty',id_b = match qb with
+  let id_b,ty',ty1,ty2 = match qb with
     | Some q ->  
   	let q = apply_post ren env (current_date ren) q in
     	let (name,t1,t2) = Term.destLambda q.a_value in
-    	Term.mkLambda (name, t1, (mkArrow t2 ty)), q.a_name
+	q.a_name,
+    	Term.mkLambda (name, t1, mkArrow t2 ty),
+	Term.mkApp (q.a_value, [| coq_true |]),
+	Term.mkApp (q.a_value, [| coq_false |])
     | None -> assert false
   in
-  CC_app (CC_case (ty', b, [br1;br2]),
+  let n = test_name Anonymous in
+  CC_app (CC_case (ty', b, [CC_lam ([n,CC_typed_binder ty1], br1);
+			    CC_lam ([n,CC_typed_binder ty2], br2)]),
 	  [CC_var (post_name id_b)])
 
 let make_if ren env (tb,cb) ren' (t1,c1) (t2,c2) c =
@@ -436,17 +441,10 @@ let make_if ren env (tb,cb) ren' (t1,c1) (t2,c2) c =
   in
   let t1,ty1 = branch c1 t1 in
   let t2,ty2 = branch c2 t2 in
-  let t1,t2 =
-    let n = test_name Anonymous in
-    CC_lam ([n,CC_untyped_binder],t1),
-    CC_lam ([n,CC_untyped_binder],t2) in
   let ty = ty1 in
   let qb = force_bool_name qb in
   let t = make_if_case ren env ty (CC_var resb,qb) (t1,t2) in
-  let t = 
-    make_let_in ren env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty)
-  in
-  t
+  make_let_in ren env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty)
 
 
 (* [make_while ren env (cphi,r,a) (tb,cb) (te,ce) c]
@@ -509,10 +507,6 @@ let make_body_while ren env phi_of a r id_phi0 id_w (tb,cb) tbl (i,c) =
       (CC_expr (constant "tt"),constant "unit") (ef,is)
   in
 
-  let t1,t2 =
-    let n = test_name Anonymous in
-    CC_lam ([n,CC_untyped_binder],t1),
-    CC_lam ([n,CC_untyped_binder],t2) in
   let b_al = current_vars ren' (get_reads eb) in
   let qb = force_bool_name qb in
   let t = make_if_case ren' env ty (CC_var resb,qb) (t1,t2) in
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 64a2910269..80399858c9 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -94,7 +94,7 @@ let ast_of_int n =
 let constr_of_int n =
   Astterm.interp_constr Evd.empty (Global.env ()) (ast_of_int n)
 
-let ast_constant loc s = <:ast< ($VAR $s) >>
+let ast_constant loc s = <:ast< (QUALID ($VAR $s)) >>
 
 let conj_assert {a_name=n;a_value=a} {a_value=b} = 
   let loc = Ast.loc a in
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 45ab72c385..950ef30b53 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -98,7 +98,7 @@ open Equality
 let nat = IndRef (coq_constant ["Init";"Datatypes"] "nat", 0)
 let lt = ConstRef (coq_constant ["Init";"Peano"] "lt")
 let well_founded = ConstRef (coq_constant ["Init";"Wf"] "well_founded")
-let z = IndRef (coq_constant ["Init";"fast_integer"] "Z", 0)
+let z = IndRef (coq_constant ["Zarith";"fast_integer"] "Z", 0)
 let and_ = IndRef (coq_constant ["Init";"Logic"] "and", 0)
 let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0)
 
@@ -107,7 +107,7 @@ let wf_nat_pattern =
   PApp (PRef well_founded, [| PRef nat; PRef lt |])
 (* ["((well_founded Z (Zwf ?1))"] *)
 let wf_z_pattern = 
-  let zwf = ConstRef (coq_constant ["correctness";"Zwf"] "Zwf") in
+  let zwf = ConstRef (coq_constant ["correctness";"ProgWf"] "Zwf") in
   PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta (Some 1) |]) |])
 (* ["(and ?1 ?2)"] *)
 let and_pattern = 
@@ -252,14 +252,9 @@ let wrap_save_named b =
   Command.save_named b;
   register pf_id None
 
-let wrap_save_anonymous_thm b id =
+let wrap_save_anonymous b id =
   let pf_id = Pfedit.get_current_proof_name () in
-  Command.save_anonymous_thm b (string_of_id id);
-  register pf_id (Some id)
-
-let wrap_save_anonymous_remark b id =
-  let pf_id = Pfedit.get_current_proof_name () in
-  Command.save_anonymous_remark b (string_of_id id);
+  Command.save_anonymous b (string_of_id id);
   register pf_id (Some id)
 
 let _ = add "SaveNamed"
@@ -272,14 +267,9 @@ let _ = add "DefinedNamed"
 		              wrap_save_named false)
     |   _  -> assert false)
 
-let _ = add "SaveAnonymousThm"
+let _ = add "SaveAnonymous"
     (function [VARG_IDENTIFIER id] -> 
        (fun () -> if not(Options.is_silent()) then show_script();
-	          wrap_save_anonymous_thm true id)
+	          wrap_save_anonymous true id)
     |   _  -> assert false)
 
-let _ = add "SaveAnonymousRmk"
-    (function [VARG_IDENTIFIER id] -> 
-        (fun () -> if not(Options.is_silent()) then show_script();
-	            wrap_save_anonymous_remark true id)
-    |   _  -> assert false)
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index c4c62b3cbe..e909d45111 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -12,10 +12,10 @@ Grammar vernac vernac : ast :=
 | extr_list   [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] ->
               [ (ExtractionRec ($LIST $l)) ]
 | extr_list   
-     [ "Extraction" options($o) stringarg($f) ne_qualidarg_list($l) "." ] 
+     [ "Extraction" stringarg($f) options($o) ne_qualidarg_list($l) "." ] 
   -> [ (ExtractionFile $o $f ($LIST $l)) ]
 | extr_module 
-     [ "Extraction" options($o) "Module" identarg($m) "." ]
+     [ "Extraction" "Module" options($o) identarg($m) "." ]
   -> [ (ExtractionModule $o $m) ]
 
 | extract_constant 
@@ -39,7 +39,7 @@ with idorstring : ast :=
 | ids_string [ stringarg($s) ] -> [ $s ]
 
 with options : ast :=
-| ext_opt_noopt [ "noopt" ] -> [ (VERNACARGLIST "noopt") ]
-| ext_op_expand [ "expand" "[" ne_qualidarg_list($l) "]" ] -> 
+| ext_opt_noopt [ "[" "noopt" "]" ] -> [ (VERNACARGLIST "noopt") ]
+| ext_op_expand [ "[" "expand" ne_qualidarg_list($l) "]" ] -> 
                 [ (VERNACARGLIST "expand" ($LIST $l)) ]
 | ext_opt_none  [ ] -> [ (VERNACARGLIST "nooption") ].
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index b0bb1ad3a9..6165910487 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -161,13 +161,13 @@ let _ =
 
 let interp_options keep modular = function
   | [VARG_STRING "noopt"] ->
-      { no_opt = true; modular = modular; 
+      { optimization = false; modular = modular; 
 	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
   | [VARG_STRING "nooption"] ->
-      { no_opt = false; modular = modular;
+      { optimization = not modular; modular = modular;
 	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
   | VARG_STRING "expand" :: l ->
-      { no_opt = false; modular = modular;
+      { optimization = not modular; modular = modular;
 	to_keep = refs_set_of_list keep; 
 	to_expand = refs_set_of_list (refs_of_vargl l) }
   | _ -> 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 4b04c4dec1..b7a07c7060 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -202,26 +202,29 @@ module Refset =
 
 type extraction_params = {
   modular : bool;       (* modular extraction *)
-  no_opt : bool;        (* no optimization at all *)
+  optimization : bool;  (* we need optimization *)
   to_keep : Refset.t;   (* globals to keep *)
   to_expand : Refset.t; (* globals to expand *)
 }
 
-let ml_subst_glob r m = 
+let subst_glob_ast r m = 
   let rec substrec = function
     | MLglob r' as t -> if r = r' then m else t
     | t -> ast_map substrec t
   in
   substrec
 
-let expand r m = function
-  | Dglob(r',t') -> Dglob(r', ml_subst_glob r m t')
+let subst_glob_decl r m = function
+  | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t')
   | d -> d
 
 let normalize = betared_ast
 
-let keep prm r t' = true
-  (* prm.no_opt || Refset.mem r prm.to_keep *)
+let expansion_test r t = false
+
+let expand prm r t = 
+  (not (Refset.mem r prm.to_keep)) &&
+  (Refset.mem r prm.to_expand || (prm.optimization && expansion_test r t))
 
 let warning_expansion r = 
   wARN (hOV 0 [< 'sTR "The constant"; 'sPC;
@@ -240,13 +243,12 @@ let rec optimize prm = function
       let t' = normalize t in [ Dglob(r,t') ]
   | Dglob(r,t) as d :: l ->
       let t' = normalize t in
-      if keep prm r t' then
-	(Dglob(r,t')) :: (optimize prm l)
-      else begin
+      if expand prm r t' then begin
 	warning_expansion r;
-	let l' = List.map (expand r t') l in
+	let l' = List.map (subst_glob_decl r t') l in
         optimize prm l'
-      end
+      end else 
+	(Dglob(r,t')) :: (optimize prm l)
 
 (*s Table for direct ML extractions. *)
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index af931b6486..f4aae3b7fc 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -45,7 +45,7 @@ module Refset : Set.S with type elt = global_reference
 
 type extraction_params = {
   modular : bool;       (* modular extraction *)
-  no_opt : bool;        (* no optimization at all *)
+  optimization : bool;  (* we need optimization *)
   to_keep : Refset.t;   (* globals to keep *)
   to_expand : Refset.t; (* globals to expand *)
 }
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index fa2384d47d..72f577a7cc 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1008,15 +1008,19 @@ let hnf env sigma c = apprec env sigma (c, empty_stack)
 
 (* A reduction function like whd_betaiota but which keeps casts
  * and does not reduce redexes containing meta-variables.
- * ASSUMES THAT APPLICATIONS ARE BINARY ONES.
- * Used in Programs.
+ * Used in Correctness.
  * Added by JCF, 29/1/98. *)
 
 let whd_programs_stack env sigma = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-      | IsApp (f,([|c|] as cl)) ->
-	  if occur_meta c then s else whrec (f, append_stack cl stack)
+      | IsApp (f,cl) ->
+	  let n = Array.length cl - 1 in
+	  let c = cl.(n) in
+	  if occur_meta c then 
+	    s 
+	  else 
+	    whrec (mkApp (f, Array.sub cl 0 n), append_stack [|c|] stack)
       | IsLambda (_,_,c) ->
           (match decomp_stack stack with
              | None -> s
-- 
cgit v1.2.3