aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend424
-rw-r--r--.depend.camlp42
-rw-r--r--Makefile7
-rw-r--r--contrib/correctness/Correctness.v9
-rw-r--r--contrib/correctness/examples/exp.v13
-rw-r--r--contrib/correctness/examples/exp_int.v8
-rw-r--r--contrib/correctness/pcic.ml5
-rw-r--r--contrib/correctness/pmisc.ml8
-rw-r--r--contrib/correctness/pmisc.mli6
-rw-r--r--contrib/correctness/pmonad.ml24
-rw-r--r--contrib/correctness/psyntax.ml42
-rw-r--r--contrib/correctness/ptactic.ml22
-rw-r--r--contrib/extraction/Extraction.v8
-rw-r--r--contrib/extraction/extract_env.ml6
-rw-r--r--contrib/extraction/mlutil.ml24
-rw-r--r--contrib/extraction/mlutil.mli2
-rw-r--r--kernel/reduction.ml12
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:58:25 +0000