aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend197
-rw-r--r--Makefile8
-rw-r--r--contrib/correctness/past.mli5
-rw-r--r--contrib/correctness/pcic.ml120
-rw-r--r--contrib/correctness/pcic.mli8
-rw-r--r--contrib/correctness/pmisc.ml18
-rw-r--r--contrib/correctness/pmisc.mli2
-rw-r--r--contrib/correctness/pmonad.ml96
-rw-r--r--contrib/correctness/pred.ml10
-rw-r--r--contrib/correctness/ptactic.ml23
-rw-r--r--contrib/correctness/putil.ml4
-rw-r--r--contrib/interface/parse.ml9
-rw-r--r--parsing/g_basevernac.ml42
-rw-r--r--parsing/g_prim.ml42
-rw-r--r--parsing/g_proofs.ml42
-rw-r--r--parsing/g_tactic.ml42
-rw-r--r--parsing/g_vernac.ml44
-rw-r--r--parsing/pcoq.ml48
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/q_coqast.ml42
-rw-r--r--toplevel/metasyntax.ml2
21 files changed, 259 insertions, 267 deletions
diff --git a/.depend b/.depend
index d119a5e88..d83d76d76 100644
--- a/.depend
+++ b/.depend
@@ -211,7 +211,8 @@ 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 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
@@ -223,8 +224,7 @@ contrib/correctness/penv.cmi: kernel/names.cmi contrib/correctness/past.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: contrib/extraction/genpp.cmi \
- kernel/names.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 \
@@ -255,12 +255,9 @@ contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \
kernel/term.cmi
contrib/extraction/extraction.cmi: kernel/environ.cmi \
contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi
-contrib/extraction/genpp.cmi: contrib/extraction/extraction.cmi \
- contrib/extraction/miniml.cmi kernel/names.cmi lib/pp.cmi \
- toplevel/vernacinterp.cmi
contrib/extraction/miniml.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi
-contrib/extraction/mlimport.cmi: kernel/names.cmi kernel/term.cmi
-contrib/extraction/mlutil.cmi: contrib/extraction/miniml.cmi kernel/names.cmi
+contrib/extraction/mlutil.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
+ kernel/term.cmi
contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi
contrib/interface/dad.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
proofs/tacmach.cmi
@@ -536,10 +533,8 @@ parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi
parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi
-parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
- toplevel/vernac.cmi
-parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
- toplevel/vernac.cmx
+parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi
+parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx
parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi
parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx
parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi
@@ -556,12 +551,12 @@ parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \
parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \
parsing/coqlib.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx \
lib/pp.cmx parsing/termast.cmx lib/util.cmx parsing/g_natsyntax.cmi
-parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi
-parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx toplevel/vernac.cmx
+parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi
+parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx
parsing/g_proofs.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \
- lib/util.cmi toplevel/vernac.cmi
+ lib/util.cmi
parsing/g_proofs.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \
- lib/util.cmx toplevel/vernac.cmx
+ lib/util.cmx
parsing/g_rsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
lib/util.cmi
@@ -569,13 +564,13 @@ parsing/g_rsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx \
lib/util.cmx
parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
- lib/pp.cmi lib/util.cmi toplevel/vernac.cmi
+ lib/pp.cmi lib/util.cmi
parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
- lib/pp.cmx lib/util.cmx toplevel/vernac.cmx
+ lib/pp.cmx lib/util.cmx
parsing/g_vernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
- lib/pp.cmi lib/util.cmi toplevel/vernac.cmi
+ lib/pp.cmi lib/util.cmi
parsing/g_vernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
- lib/pp.cmx lib/util.cmx toplevel/vernac.cmx
+ lib/pp.cmx lib/util.cmx
parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
lib/util.cmi parsing/g_zsyntax.cmi
@@ -585,9 +580,9 @@ parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
parsing/lexer.cmo: parsing/lexer.cmi
parsing/lexer.cmx: parsing/lexer.cmi
parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
- lib/util.cmi toplevel/vernac.cmi parsing/pcoq.cmi
+ lib/util.cmi parsing/pcoq.cmi
parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
- lib/util.cmx toplevel/vernac.cmx parsing/pcoq.cmi
+ lib/util.cmx parsing/pcoq.cmi
parsing/pretty.cmo: pretyping/classops.cmi kernel/declarations.cmi \
library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \
@@ -1248,12 +1243,12 @@ toplevel/metasyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
parsing/coqast.cmi parsing/egrammar.cmi parsing/esyntax.cmi \
parsing/extend.cmi library/lib.cmi library/libobject.cmi \
library/library.cmi parsing/pcoq.cmi lib/pp.cmi library/summary.cmi \
- lib/util.cmi toplevel/vernac.cmi toplevel/metasyntax.cmi
+ lib/util.cmi toplevel/metasyntax.cmi
toplevel/metasyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
parsing/coqast.cmx parsing/egrammar.cmx parsing/esyntax.cmx \
parsing/extend.cmx library/lib.cmx library/libobject.cmx \
library/library.cmx parsing/pcoq.cmx lib/pp.cmx library/summary.cmx \
- lib/util.cmx toplevel/vernac.cmx toplevel/metasyntax.cmi
+ lib/util.cmx toplevel/metasyntax.cmi
toplevel/minicoq.cmo: kernel/declarations.cmi toplevel/fhimsg.cmi \
parsing/g_minicoq.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \
@@ -1358,22 +1353,16 @@ 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/past.cmo: parsing/coqast.cmi kernel/names.cmi \
- contrib/correctness/ptype.cmi kernel/term.cmi \
- contrib/correctness/past.cmi
-contrib/correctness/past.cmx: parsing/coqast.cmx kernel/names.cmx \
- contrib/correctness/ptype.cmx kernel/term.cmx \
- contrib/correctness/past.cmi
contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \
- library/declare.cmi kernel/names.cmi library/nametab.cmi \
- contrib/correctness/past.cmi contrib/correctness/pmisc.cmi \
- toplevel/record.cmi kernel/term.cmi lib/util.cmi \
- contrib/correctness/pcic.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 kernel/names.cmx library/nametab.cmx \
- contrib/correctness/past.cmx contrib/correctness/pmisc.cmx \
- toplevel/record.cmx kernel/term.cmx lib/util.cmx \
- contrib/correctness/pcic.cmi
+ 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 \
@@ -1381,9 +1370,9 @@ contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.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.cmx contrib/correctness/penv.cmx \
+ contrib/correctness/past.cmi contrib/correctness/penv.cmx \
contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
- contrib/correctness/prename.cmx contrib/correctness/ptype.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 \
@@ -1392,9 +1381,9 @@ contrib/correctness/pdb.cmo: library/declare.cmi library/global.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.cmx \
+ kernel/names.cmx library/nametab.cmx contrib/correctness/past.cmi \
contrib/correctness/penv.cmx contrib/correctness/perror.cmx \
- contrib/correctness/ptype.cmx kernel/sign.cmx kernel/term.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 \
@@ -1409,8 +1398,8 @@ contrib/correctness/penv.cmo: toplevel/himsg.cmi library/lib.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.cmx contrib/correctness/perror.cmx \
- contrib/correctness/pmisc.cmx lib/pp.cmx contrib/correctness/ptype.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 \
@@ -1420,21 +1409,21 @@ contrib/correctness/perror.cmo: library/declare.cmi kernel/evd.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.cmx contrib/correctness/peffect.cmx lib/pp.cmx \
- contrib/correctness/ptype.cmx contrib/correctness/putil.cmx \
+ contrib/correctness/past.cmi contrib/correctness/peffect.cmx lib/pp.cmx \
+ contrib/correctness/ptype.cmi contrib/correctness/putil.cmx \
kernel/reduction.cmx kernel/term.cmx lib/util.cmx \
contrib/correctness/perror.cmi
contrib/correctness/pextract.cmo: parsing/ast.cmi kernel/evd.cmi \
- contrib/extraction/genpp.cmi toplevel/himsg.cmi library/library.cmi \
- kernel/names.cmi library/nametab.cmi contrib/extraction/ocaml.cmi \
+ toplevel/himsg.cmi library/library.cmi kernel/names.cmi \
+ library/nametab.cmi contrib/extraction/ocaml.cmi \
contrib/correctness/past.cmi contrib/correctness/penv.cmi lib/pp.cmi \
lib/pp_control.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 \
- contrib/extraction/genpp.cmx toplevel/himsg.cmx library/library.cmx \
- kernel/names.cmx library/nametab.cmx contrib/extraction/ocaml.cmx \
- contrib/correctness/past.cmx contrib/correctness/penv.cmx lib/pp.cmx \
+ toplevel/himsg.cmx library/library.cmx kernel/names.cmx \
+ library/nametab.cmx contrib/extraction/ocaml.cmx \
+ contrib/correctness/past.cmi contrib/correctness/penv.cmx lib/pp.cmx \
lib/pp_control.cmx contrib/correctness/putil.cmx kernel/reduction.cmx \
lib/system.cmx kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx \
contrib/correctness/pextract.cmi
@@ -1454,11 +1443,11 @@ contrib/correctness/pmlize.cmo: parsing/coqlib.cmi kernel/evd.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.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.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
@@ -1468,17 +1457,17 @@ contrib/correctness/pmonad.cmo: kernel/names.cmi contrib/correctness/past.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.cmx \
+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.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.cmx lib/pp.cmx kernel/reduction.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 \
@@ -1502,11 +1491,11 @@ contrib/correctness/psyntax.cmo: parsing/ast.cmi parsing/astterm.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.cmx parsing/pcoq.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.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 \
@@ -1520,32 +1509,28 @@ contrib/correctness/ptactic.cmo: toplevel/command.cmi library/declare.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 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/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.cmx pretyping/pattern.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 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/ptype.cmo: kernel/names.cmi \
- contrib/correctness/peffect.cmi kernel/term.cmi \
- contrib/correctness/ptype.cmi
-contrib/correctness/ptype.cmx: kernel/names.cmx \
- contrib/correctness/peffect.cmx kernel/term.cmx \
- contrib/correctness/ptype.cmi
+ 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 \
@@ -1558,12 +1543,12 @@ contrib/correctness/ptyping.cmo: parsing/ast.cmi parsing/astterm.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.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.cmx contrib/correctness/putil.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 \
@@ -1573,10 +1558,10 @@ contrib/correctness/putil.cmo: parsing/coqlib.cmi kernel/names.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.cmx pretyping/pattern.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.cmx kernel/term.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 \
@@ -1587,11 +1572,11 @@ contrib/correctness/pwp.cmo: kernel/evd.cmi library/global.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.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.cmx contrib/correctness/ptyping.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 \
@@ -1611,39 +1596,25 @@ contrib/extraction/extract_env.cmx: parsing/astterm.cmx kernel/evd.cmx \
contrib/extraction/extraction.cmo: kernel/closure.cmi kernel/declarations.cmi \
kernel/environ.cmi kernel/evd.cmi library/global.cmi lib/gmap.cmi \
kernel/inductive.cmi kernel/instantiate.cmi contrib/extraction/miniml.cmi \
- contrib/extraction/mlimport.cmi contrib/extraction/mlutil.cmi \
- kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/term.cmi \
- pretyping/typing.cmi lib/util.cmi contrib/extraction/extraction.cmi
+ contrib/extraction/mlutil.cmi kernel/names.cmi lib/pp.cmi \
+ kernel/reduction.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
+ contrib/extraction/extraction.cmi
contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \
kernel/environ.cmx kernel/evd.cmx library/global.cmx lib/gmap.cmx \
kernel/inductive.cmx kernel/instantiate.cmx contrib/extraction/miniml.cmi \
- contrib/extraction/mlimport.cmx contrib/extraction/mlutil.cmx \
- kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/term.cmx \
- pretyping/typing.cmx lib/util.cmx contrib/extraction/extraction.cmi
-contrib/extraction/genpp.cmo: kernel/environ.cmi \
- contrib/extraction/extraction.cmi contrib/extraction/genpp.cmi \
- library/global.cmi contrib/extraction/miniml.cmi \
- contrib/extraction/mlimport.cmi kernel/names.cmi library/nametab.cmi \
- lib/pp.cmi lib/pp_control.cmi lib/system.cmi lib/util.cmi \
- toplevel/vernacinterp.cmi contrib/extraction/genpp.cmi
-contrib/extraction/genpp.cmx: kernel/environ.cmx \
- contrib/extraction/extraction.cmx contrib/extraction/genpp.cmx \
- library/global.cmx contrib/extraction/miniml.cmi \
- contrib/extraction/mlimport.cmx kernel/names.cmx library/nametab.cmx \
- lib/pp.cmx lib/pp_control.cmx lib/system.cmx lib/util.cmx \
- toplevel/vernacinterp.cmx contrib/extraction/genpp.cmi
-contrib/extraction/mlimport.cmo: library/declare.cmi lib/gmap.cmi \
- library/lib.cmi library/libobject.cmi kernel/names.cmi \
- library/nametab.cmi lib/pp.cmi parsing/printer.cmi library/summary.cmi \
- kernel/term.cmi contrib/extraction/mlimport.cmi
-contrib/extraction/mlimport.cmx: library/declare.cmx lib/gmap.cmx \
- library/lib.cmx library/libobject.cmx kernel/names.cmx \
- library/nametab.cmx lib/pp.cmx parsing/printer.cmx library/summary.cmx \
- kernel/term.cmx contrib/extraction/mlimport.cmi
-contrib/extraction/mlutil.cmo: contrib/extraction/miniml.cmi kernel/names.cmi \
- lib/util.cmi contrib/extraction/mlutil.cmi
-contrib/extraction/mlutil.cmx: contrib/extraction/miniml.cmi kernel/names.cmx \
- lib/util.cmx contrib/extraction/mlutil.cmi
+ contrib/extraction/mlutil.cmx kernel/names.cmx lib/pp.cmx \
+ kernel/reduction.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
+ contrib/extraction/extraction.cmi
+contrib/extraction/mlutil.cmo: kernel/declarations.cmi library/global.cmi \
+ library/lib.cmi library/libobject.cmi contrib/extraction/miniml.cmi \
+ kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
+ library/summary.cmi kernel/term.cmi lib/util.cmi \
+ toplevel/vernacinterp.cmi contrib/extraction/mlutil.cmi
+contrib/extraction/mlutil.cmx: kernel/declarations.cmx library/global.cmx \
+ library/lib.cmx library/libobject.cmx contrib/extraction/miniml.cmi \
+ kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
+ library/summary.cmx kernel/term.cmx lib/util.cmx \
+ toplevel/vernacinterp.cmx contrib/extraction/mlutil.cmi
contrib/extraction/ocaml.cmo: kernel/environ.cmi library/global.cmi \
contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
kernel/names.cmi lib/pp.cmi lib/pp_control.cmi kernel/term.cmi \
diff --git a/Makefile b/Makefile
index 75a5a1ef3..381b9cfb9 100644
--- a/Makefile
+++ b/Makefile
@@ -142,9 +142,8 @@ EXTRACTIONCMO=contrib/extraction/mlutil.cmo contrib/extraction/ocaml.cmo \
contrib/extraction/extraction.cmo \
contrib/extraction/extract_env.cmo
-CORRECTNESS=contrib/correctness/pmisc.cmo \
+CORRECTNESSCMO=contrib/correctness/pmisc.cmo \
contrib/correctness/peffect.cmo contrib/correctness/prename.cmo \
- contrib/correctness/ptype.cmo contrib/correctness/past.cmo \
contrib/correctness/perror.cmo contrib/correctness/penv.cmo \
contrib/correctness/putil.cmo contrib/correctness/pdb.cmo \
contrib/correctness/pcic.cmo contrib/correctness/pmonad.cmo \
@@ -202,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
-# $(CORRECTNESS)
+# $(CORRECTNESSCMO)
CMA=$(CLIBS) $(CAMLP4OBJS)
CMXA=$(CMA:.cma=.cmxa)
@@ -278,6 +277,9 @@ parsing: $(PARSING)
pretyping: $(PRETYPING)
toplevel: $(TOPLEVEL)
+extraction: $(EXTRACTIONCMO)
+correctness: $(CORRECTNESSCMO)
+
# special binaries for debugging
bin/coq-extraction: $(COQMKTOP) $(CMO) $(USERTACCMO) $(EXTRACTIONCMO)
diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
index 5db3c87b6..7696c6698 100644
--- a/contrib/correctness/past.mli
+++ b/contrib/correctness/past.mli
@@ -87,11 +87,10 @@ type cc_binder = variable * cc_bind_type
type cc_term =
| CC_var of variable
- | CC_letin of
- bool * cc_type * cc_binder list * (cc_term * Term.case_info) * cc_term
+ | CC_letin of bool * cc_type * cc_binder list * cc_term * cc_term
| CC_lam of cc_binder list * cc_term
| CC_app of cc_term * cc_term list
| CC_tuple of bool * cc_type list * cc_term list
- | CC_case of cc_type * (cc_term * Term.case_info) * cc_term list
+ | CC_case of cc_type * cc_term * cc_term list
| CC_expr of Term.constr
| CC_hole of cc_type
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 49871b23a..170a56b28 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -13,6 +13,8 @@
open Names
open Term
open Declarations
+open Sign
+open Rawterm
open Pmisc
open Past
@@ -87,86 +89,112 @@ let sig_n n =
mind_entry_consnames = [ cname ];
mind_entry_lc = [ lc ] } ] }
-let tuple_name dep n =
+let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "pair",0),1)
+let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "exist",0),1)
+
+let tuple_ref dep n =
if n = 2 & not dep then
- "pair"
+ pair
else
let n = n - (if dep then 1 else 0) in
if dep then
if n = 1 then
- "exist"
+ exist
else begin
let name = Printf.sprintf "exist_%d" n in
- if not (tuple_exists (id_of_string name)) then ignore (sig_n n);
- name
+ let id = id_of_string name in
+ if not (tuple_exists id) then ignore (sig_n n);
+ Nametab.sp_of_id CCI id
end
else begin
let name = Printf.sprintf "Build_tuple_%d" n in
- if not (tuple_exists (id_of_string name)) then tuple_n n;
- name
+ let id = id_of_string name in
+ if not (tuple_exists id) then tuple_n n;
+ Nametab.sp_of_id CCI id
end
(* Binders. *)
-let trad_binding bl =
- List.map (function
- (id,CC_untyped_binder) -> (id,isevar)
- | (id,CC_typed_binder ty) -> (id,ty)) bl
-
-let lambda_of_bl bl c =
- let b = trad_binding bl in n_lambda c (List.rev b)
+let trad_binder avoid nenv = function
+ | CC_untyped_binder -> RHole None
+ | CC_typed_binder ty -> Detyping.detype avoid nenv ty
+
+let rec push_vars avoid nenv = function
+ | [] -> ([],avoid,nenv)
+ | (id,b) :: bl ->
+ let b' = trad_binder avoid nenv b in
+ let bl',avoid',nenv' =
+ push_vars (id :: avoid) (add_name (Name id) nenv) bl
+ in
+ ((id,b') :: bl', avoid', nenv')
+
+let rec raw_lambda bl v = match bl with
+ | [] ->
+ v
+ | (id,ty) :: bl' ->
+ RLambda (dummy_loc, Name id, ty, raw_lambda bl' v)
(* The translation itself is quite easy.
- letin are translated into Cases construtions *)
+ letin are translated into Cases constructions *)
-let constr_of_prog p =
- let rec trad = function
- | CC_var id -> mkVar id
+let rawconstr_of_prog p =
+ let rec trad avoid nenv = function
+ | CC_var id ->
+ RVar (dummy_loc, id)
- (* optimisation : let x = <constr> in e2 => e2[x<-constr] *)
- | CC_letin (_,_,[id,_],(CC_expr c,_),e2) ->
+ (*i optimisation : let x = <constr> in e2 => e2[x<-constr]
+ | CC_letin (_,_,[id,_],CC_expr c,e2) ->
real_subst_in_constr [id,c] (trad e2)
+ i*)
- | CC_letin (_,_,([_] as b),(e1,_),e2) ->
- let c = trad e1 and c2 = trad e2 in
- Term.applist (lambda_of_bl b c2, [c])
+ | CC_letin (_,_,([_] as b),e1,e2) ->
+ let (b',avoid',nenv') = push_vars avoid nenv b in
+ let c1 = trad avoid nenv e1
+ and c2 = trad avoid' nenv' e2 in
+ RApp (dummy_loc, raw_lambda b' c2, [c1])
- | CC_letin (dep,ty,bl,(e,info),e1) ->
- let c1 = trad e1
- and c = trad e in
- let l = [| lambda_of_bl bl c1 |] in
- Term.mkMutCase (info, ty, c, l)
+ | CC_letin (dep,ty,bl,e1,e2) ->
+ let (bl',avoid',nenv') = push_vars avoid nenv bl in
+ let c1 = trad avoid nenv e1
+ and c2 = trad avoid' nenv' e2 in
+ ROldCase (dummy_loc, false, None, c1, [| raw_lambda bl' c2 |])
| CC_lam (bl,e) ->
- let c = trad e in lambda_of_bl bl c
+ let bl',avoid',nenv' = push_vars avoid nenv bl in
+ let c = trad avoid' nenv' e in
+ raw_lambda bl' c
| CC_app (f,args) ->
- let c = trad f
- and cargs = List.map trad args in
- Term.applist (c,cargs)
+ let c = trad avoid nenv f
+ and cargs = List.map (trad avoid nenv) args in
+ RApp (dummy_loc, c, cargs)
- | CC_tuple (_,_,[e]) -> trad e
+ | CC_tuple (_,_,[e]) ->
+ trad avoid nenv e
| CC_tuple (false,_,[e1;e2]) ->
- let c1 = trad e1
- and c2 = trad e2 in
- Term.applist (constant "pair", [isevar;isevar;c1;c2])
+ let c1 = trad avoid nenv e1
+ and c2 = trad avoid nenv e2 in
+ RApp (dummy_loc, RRef (dummy_loc,pair), [RHole None;RHole None;c1;c2])
| CC_tuple (dep,tyl,l) ->
let n = List.length l in
- let cl = List.map trad l in
- let name = tuple_name dep n in
+ let cl = List.map (trad avoid nenv) l in
+ let tuple = tuple_ref dep n in
+ let tyl = List.map (Detyping.detype avoid nenv) tyl in
let args = tyl @ cl in
- Term.applist (constant name,args)
+ RApp (dummy_loc, RRef (dummy_loc, tuple), args)
- | CC_case (ty,(b,info),el) ->
- let c = trad b in
- let cl = List.map trad el in
- mkMutCase (info, ty, c, Array.of_list cl)
+ | CC_case (_,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)
- | CC_expr c -> c
+ | CC_expr c ->
+ Detyping.detype avoid nenv c
- | CC_hole c -> make_hole c
+ | CC_hole c ->
+ RCast (dummy_loc, RHole None, Detyping.detype avoid nenv c)
in
- trad p
+ trad [] empty_names_context p
diff --git a/contrib/correctness/pcic.mli b/contrib/correctness/pcic.mli
index 21c3839d9..f0b629071 100644
--- a/contrib/correctness/pcic.mli
+++ b/contrib/correctness/pcic.mli
@@ -8,13 +8,13 @@
(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
-(* $Id$ *)
+(*i $Id$ i*)
open Past
-open Term
+open Rawterm
-(* transforms intermediate functional programs into CIC terms *)
+(* transforms intermediate functional programs into (raw) CIC terms *)
-val constr_of_prog : cc_term -> constr
+val rawconstr_of_prog : cc_term -> rawconstr
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index f25541961..77356e17c 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -17,6 +17,8 @@ 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
@@ -159,22 +161,20 @@ let is_connective id =
(* [conj i s] constructs the conjunction of two constr *)
-let conj i s =
- Term.applist (constant "and", [i; s])
-
+let conj i s = Term.applist (constant "and", [i; s])
-(* [n_mkNamedProd v [xn,tn;...;x1,t1]] constructs the type (x1:t1)...(xn:tn)v
- *)
+(* [n_mkNamedProd v [xn,tn;...;x1,t1]] constructs the type
+ [(x1:t1)...(xn:tn)v] *)
let rec n_mkNamedProd v = function
- [] -> v
- | (id,ty)::rem -> n_mkNamedProd (Term.mkNamedProd id ty v) rem
+ | [] -> v
+ | (id,ty) :: rem -> n_mkNamedProd (Term.mkNamedProd id ty v) rem
(* [n_lambda v [xn,tn;...;x1,t1]] constructs the type [x1:t1]...[xn:tn]v *)
let rec n_lambda v = function
- [] -> v
- | (id,ty)::rem -> n_lambda (Term.mkNamedLambda id ty v) rem
+ | [] -> v
+ | (id,ty) :: rem -> n_lambda (Term.mkNamedLambda id ty v) rem
(* [abstract env idl c] constructs [x1]...[xn]c where idl = [x1;...;xn] *)
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index f486d0d4e..96519ee9f 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -15,6 +15,8 @@ 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
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml
index 30892ee4c..6dbf1e460 100644
--- a/contrib/correctness/pmonad.ml
+++ b/contrib/correctness/pmonad.ml
@@ -35,17 +35,17 @@ open Peffect
*)
let product_name = function
- 2 -> "prod"
+ | 2 -> "prod"
| n -> Printf.sprintf "tuple_%d" n
let dep_product_name = function
- 1 -> "sig"
+ | 1 -> "sig"
| n -> Printf.sprintf "sig_%d" n
let product ren env before lo = function
- None -> (* non dependent case *)
+ | None -> (* non dependent case *)
begin match lo with
- [_,v] -> v
+ | [_,v] -> v
| _ ->
let s = product_name (List.length lo) in
Term.applist (constant s, List.map snd lo)
@@ -88,8 +88,7 @@ let rec abstract_post ren env (e,q) =
and prod ren env g =
List.map
- (fun id ->
- (current_var ren id,trad_type_in_env ren env id))
+ (fun id -> (current_var ren id, trad_type_in_env ren env id))
g
and input ren env e =
@@ -124,7 +123,7 @@ and trad_ml_type_v ren env = function
let bl',ren',env' =
List.fold_left
(fun (bl,ren,env) b -> match b with
- (id,BindType ((Ref _ | Array _) as v)) ->
+ | (id,BindType ((Ref _ | Array _) as v)) ->
let env' = add (id,v) env in
let ren' = initial_renaming env' in
(bl,ren',env')
@@ -145,7 +144,7 @@ and trad_ml_type_v ren env = function
(apply_pre ren env (anonymous_pre false c)).p_value
and trad_imp_type ren env = function
- Ref v -> trad_ml_type_v ren env v
+ | Ref v -> trad_ml_type_v ren env v
| Array (c,v) -> Term.applist (constant "array",
[c; trad_ml_type_v ren env v])
| _ -> invalid_arg "Monad.trad_imp_type"
@@ -166,10 +165,9 @@ let binding_of_alist ren env al =
(* [make_abs bl t p] abstracts t w.r.t binding list bl., that is
* [x1:t1]...[xn:tn]t. Returns t if the binding is empty. *)
-let make_abs bl t =
- match bl with
- [] -> t
- | _ -> CC_lam (bl, t)
+let make_abs bl t = match bl with
+ | [] -> t
+ | _ -> CC_lam (bl, t)
(* [result_tuple ren before env (res,v) (ef,q)] constructs the tuple
@@ -180,21 +178,21 @@ let make_abs bl t =
* if there is no yi and no post-condition, it is simplified in res itself.
*)
-let make_tuple l q ren env before =
- match l with
- [e,_] when q = None -> e
- | _ ->
- let tl = List.map snd l in
- let dep,h,th = match q with
- None -> false,[],[]
- | Some c ->
- let args = List.map (fun (e,_) -> constr_of_prog e) l in
- let c = apply_post ren env before c in
- true,
- [ CC_hole (Term.applist (c.a_value, args)) ], (* hole *)
- [ c.a_value ] (* type of the hole *)
- in
- CC_tuple (dep, tl @ th, (List.map fst l) @ h)
+let make_tuple l q ren env before = match l with
+ | [e,_] when q = None ->
+ e
+ | _ ->
+ let tl = List.map snd l in
+ let dep,h,th = match q with
+ | None -> false,[],[]
+ | Some c ->
+ let args = List.map (fun (e,_) -> constr_of_prog e) l in
+ let c = apply_post ren env before c in
+ true,
+ [ CC_hole (Term.applist (c.a_value, args)) ], (* hole *)
+ [ c.a_value ] (* type of the hole *)
+ in
+ CC_tuple (dep, tl @ th, (List.map fst l) @ h)
let result_tuple ren before env (res,v) (ef,q) =
let ids = get_writes ef in
@@ -202,7 +200,7 @@ let result_tuple ren before env (res,v) (ef,q) =
(List.map (fun id ->
let id' = current_var ren id in
CC_var id', trad_type_in_env ren env id) ids)
- @[res,v]
+ @ [res,v]
in
let q = abstract_post ren env (ef,q) in
make_tuple lo q ren env before,
@@ -266,25 +264,25 @@ let abs_pre ren env (t,ty) pl =
let make_block ren env finish bl =
let rec rec_block ren result = function
- [] ->
+ | [] ->
finish ren result
- | (Assert c) :: block ->
- let t,ty = rec_block ren result block in
- let c = apply_assert ren env c in
- let p = { p_assert = true; p_name = c.a_name; p_value = c.a_value } in
- let_in_pre ty p t, ty
- | (Label s) :: block ->
- let ren' = push_date ren s in
- rec_block ren' result block
- | (Statement (te,info)) :: block ->
- let (_,tye),efe,pe,qe = info in
- let w = get_writes efe in
- let ren' = next ren w in
- let id = result_id in
- let tye = trad_ml_type_v ren env tye in
- let t = rec_block ren' (Some (id,tye)) block in
- make_let_in ren env te pe (current_vars ren' w,qe) (id,tye) t,
- snd t
+ | (Assert c) :: block ->
+ let t,ty = rec_block ren result block in
+ let c = apply_assert ren env c in
+ let p = { p_assert = true; p_name = c.a_name; p_value = c.a_value } in
+ let_in_pre ty p t, ty
+ | (Label s) :: block ->
+ let ren' = push_date ren s in
+ rec_block ren' result block
+ | (Statement (te,info)) :: block ->
+ let (_,tye),efe,pe,qe = info in
+ let w = get_writes efe in
+ let ren' = next ren w in
+ let id = result_id in
+ let tye = trad_ml_type_v ren env tye in
+ let t = rec_block ren' (Some (id,tye)) block in
+ make_let_in ren env te pe (current_vars ren' w,qe) (id,tye) t,
+ snd t
in
let t,_ = rec_block ren None bl in
t
@@ -333,11 +331,7 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c =
let ((_,tvf),ef,pf,qf) = cf in
let (_,eapp,papp,qapp) = capp in
let ((_,v),e,p,q) = c in
-
- let bl = Util.map_succeed
- (function b -> if is_ref_binder b then failwith "caught" else b)
- bl
- in
+ let bl = List.filter (fun b -> not (is_ref_binder b)) bl in
let recur = is_recursive env tf in
let before = current_date ren in
let ren'' = next ren' (get_writes ef) in
diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml
index 02c84cf00..d6f9e0e72 100644
--- a/contrib/correctness/pred.ml
+++ b/contrib/correctness/pred.ml
@@ -29,23 +29,23 @@ let is_eta_redex bl al =
Invalid_argument("List.for_all2") -> false
let rec red = function
- CC_letin (dep, ty, bl, (e1,info), e2) ->
+ CC_letin (dep, ty, bl, e1, e2) ->
begin match red e2 with
CC_tuple (false,tl,al) ->
if is_eta_redex bl al then
red e1
else
- CC_letin (dep, ty, bl, (red e1,info),
+ CC_letin (dep, ty, bl, red e1,
CC_tuple (false,tl,List.map red al))
- | e -> CC_letin (dep, ty, bl, (red e1,info), e)
+ | e -> CC_letin (dep, ty, bl, red e1, e)
end
| CC_lam (bl, e) ->
CC_lam (bl, red e)
| CC_app (e, al) ->
CC_app (red e, List.map red al)
- | CC_case (ty, (e1,info), el) ->
- CC_case (ty, (red e1,info), List.map red el)
+ | CC_case (ty, e1, el) ->
+ CC_case (ty, red e1, List.map red el)
| CC_tuple (dep, tl, al) ->
CC_tuple (dep, tl, List.map red al)
| e -> e
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 5eb03d23e..d92d8524b 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -13,6 +13,7 @@
open Pp
open Names
open Term
+open Pretyping
open Pfedit
open Vernacentries
@@ -61,18 +62,15 @@ let coqast_of_prog p =
deb_mess
[< 'fNL; 'sTR"Pcic.constr_of_prog: Traduction cc_term -> constr...";
'fNL >];
- let c = Pcic.constr_of_prog cc in
- deb_mess (Printer.prterm c);
+ let r = Pcic.rawconstr_of_prog cc in
+ deb_mess (Printer.pr_rawterm r);
(* 6. résolution implicites *)
deb_mess [< 'fNL; 'sTR"Résolution implicites (? => Meta(n))..."; 'fNL >];
- let c = c in
- (*i WAS
- (ise_resolve false (Evd.mt_evd()) [] (gLOB(initial_sign())) c)._VAL in
- i*)
- deb_mess (Printer.prterm c);
+ let oc = understand_gen_tcc Evd.empty (Global.env()) [] [] None r in
+ deb_mess (Printer.prterm (snd oc));
- p,c,ty,v
+ p,oc,ty,v
(* [automatic : tactic]
*
@@ -97,8 +95,6 @@ open Tactics
open Tacticals
open Equality
-let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
-
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")
@@ -201,7 +197,7 @@ let (automatic : tactic) =
let correctness s p opttac =
Pmisc.reset_names();
- let p,c,cty,v = coqast_of_prog p in
+ let p,oc,cty,v = coqast_of_prog p in
let env = Global.env () in
let sign = Global.named_context () in
let sigma = Evd.empty in
@@ -211,10 +207,9 @@ let correctness s p opttac =
Penv.new_edited id (v,p);
if !debug then show_open_subgoals();
deb_mess [< 'sTR"Pred.red_cci: Réduction..."; 'fNL >];
- let c = Pred.red_cci c in
+ let oc = let (mm,c) = oc in (mm, Pred.red_cci c) in
deb_mess [< 'sTR"APRES REDUCTION :"; 'fNL >];
- deb_mess (Printer.prterm c);
- let oc = [],c in (* TODO: quid des existentielles ici *)
+ deb_mess (Printer.prterm (snd oc));
let tac = (tclTHEN (Refine.refine_tac oc) automatic) in
let tac = match opttac with
| None -> tac
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index 2f86d355e..e227a4459 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -264,7 +264,7 @@ and pp_binder = function
let rec pp_cc_term = function
CC_var id -> pr_id id
- | CC_letin (_,_,bl,(c,_),c1) ->
+ | CC_letin (_,_,bl,c,c1) ->
hOV 0 [< hOV 2 [< 'sTR"let ";
prlist_with_sep (fun () -> [< 'sTR"," >])
(fun (id,_) -> pr_id id) bl;
@@ -287,7 +287,7 @@ let rec pp_cc_term = function
prlist_with_sep (fun () -> [< 'sTR","; 'cUT >])
pp_cc_term cl;
'sTR")" >]
- | CC_case (_,(b,_),[e1;e2]) ->
+ | CC_case (_,b,[e1;e2]) ->
hOV 0 [< 'sTR"if "; pp_cc_term b; 'sTR" then"; 'fNL;
'sTR" "; hOV 0 (pp_cc_term e1); 'fNL;
'sTR"else"; 'fNL;
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index f1f04a2df..7648e7922 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -190,7 +190,7 @@ let parse_string_action reqid phylum char_stream string_list =
P_c
(xlate_vernac
(execute_when_necessary
- (Gram.Entry.parse Pcoq.Vernac.vernac_eoi (Gram.parsable char_stream))))
+ (Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream))))
| "TACTIC_COM" ->
P_t
(xlate_tactic (Gram.Entry.parse Pcoq.Tactic.tactic_eoi
@@ -223,9 +223,10 @@ let parse_string_action reqid phylum char_stream string_list =
let quiet_parse_string_action char_stream =
- try let _ =
- Gram.Entry.parse Pcoq.Vernac.vernac_eoi (Gram.parsable char_stream) in
- ()
+ try
+ let _ =
+ Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream) in
+ ()
with
| _ -> flush_until_end_of_stream char_stream; ();;
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index cdfb55478..4abce12f3 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -13,7 +13,7 @@
open Coqast
open Pcoq
-open Vernac
+open Vernac_
GEXTEND Gram
GLOBAL: identarg ne_identarg_list numarg ne_numarg_list numarg_list
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 05f4dc42e..414c8eb0a 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -93,7 +93,7 @@ GEXTEND Gram
| ":"; IDENT "tactic" ->
let _ = set_default_action_parser Tactic.tactic in Id(loc,"AST")
| ":"; IDENT "vernac" ->
- let _ = set_default_action_parser Vernac.vernac in Id(loc,"AST")
+ let _ = set_default_action_parser Vernac_.vernac in Id(loc,"AST")
| -> Id(loc,"AST") ]]
;
END
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index efd6a5de2..6903293bb 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -14,7 +14,7 @@ open Pcoq
open Pp
open Tactic
open Util
-open Vernac
+open Vernac_
(* Proof commands *)
GEXTEND Gram
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f26034c91..7aadc305d 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -298,7 +298,7 @@ GEXTEND Gram
<:ast< (StartProof "LETTOP" $id $c) >>
| _ -> <:ast< (LETCUT (LETDECL ($LIST $llc))) >>)
| IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And";
- tb = Vernac.theorem_body; "Qed" ->
+ tb = Vernac_.theorem_body; "Qed" ->
(match llc with
| [Coqast.Node(_,"LETTOPCLAUSE",[id;c])] ->
<:ast< (TheoremProof "LETTOP" $id $c $tb) >>
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f1cae2458..13a9ca9fb 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -14,7 +14,7 @@ open Pcoq
open Pp
open Tactic
open Util
-open Vernac
+open Vernac_
(* Rem: do not join the different GEXTEND into one, it breaks native *)
(* compilation on PowerPC and Sun architectures *)
@@ -280,7 +280,7 @@ GEXTEND Gram
| bl = simple_binders -> bl ] ]
;
rec_constr:
- [ [ c = Vernac.identarg -> <:ast< (VERNACARGLIST $c) >>
+ [ [ c = Vernac_.identarg -> <:ast< (VERNACARGLIST $c) >>
| -> <:ast< (VERNACARGLIST) >> ] ]
;
gallina_ext:
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 22fde9548..833f8a505 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -338,7 +338,7 @@ module Tactic =
end
-module Vernac =
+module Vernac_ =
struct
let uvernac = snd (get_univ "vernac")
let gec s =
@@ -405,7 +405,7 @@ let main_entry = Gram.Entry.create "vernac"
GEXTEND Gram
main_entry:
- [ [ a = Vernac.vernac -> Some a | EOI -> None ] ]
+ [ [ a = Vernac_.vernac -> Some a | EOI -> None ] ]
;
END
@@ -414,7 +414,7 @@ END
open Prim
open Constr
open Tactic
-open Vernac
+open Vernac_
(* current file and toplevel/vernac.ml *)
@@ -446,7 +446,7 @@ let _ = define_quotation false "ast" ast in ()
let constr_parser = ref Constr.constr
let tactic_parser = ref Tactic.tactic
-let vernac_parser = ref Vernac.vernac
+let vernac_parser = ref Vernac_.vernac
let update_constr_parser p = constr_parser := p
let update_tactic_parser p = tactic_parser := p
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e64088862..7044801fa 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -159,7 +159,7 @@ module Tactic :
val with_binding_list : Coqast.t Gram.Entry.e
end
-module Vernac :
+module Vernac_ :
sig
val identarg : Coqast.t Gram.Entry.e
val ne_identarg_list : Coqast.t list Gram.Entry.e
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 0b6e92a43..e8ee0c67d 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -124,7 +124,7 @@ let f e =
let _ =
Quotation.add "constr" (f Pcoq.Constr.constr_eoi);
Quotation.add "tactic" (f Pcoq.Tactic.tactic_eoi);
- Quotation.add "vernac" (f Pcoq.Vernac.vernac_eoi);
+ Quotation.add "vernac" (f Pcoq.Vernac_.vernac_eoi);
Quotation.add "ast" (f Pcoq.Prim.ast_eoi);
Quotation.default := "constr"
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 163f2a16d..ec311d9ae 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -26,7 +26,7 @@ open Summary
(* Done here to get parsing/g_*.ml4 non dependent from kernel *)
let constr_parser_with_glob = map_entry Astterm.globalize_constr Constr.constr
let tactic_parser_with_glob = map_entry Astterm.globalize_ast Tactic.tactic
-let vernac_parser_with_glob = map_entry Astterm.globalize_ast Vernac.vernac
+let vernac_parser_with_glob = map_entry Astterm.globalize_ast Vernac_.vernac
(* This updates default parsers for Grammar actions and Syntax *)
(* patterns by inserting globalization *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 13:48:41 +0000