diff options
| author | delahaye | 2000-05-03 17:31:07 +0000 |
|---|---|---|
| committer | delahaye | 2000-05-03 17:31:07 +0000 |
| commit | fc38a7d8f3d2a47aa8eee570747568335f3ffa19 (patch) | |
| tree | 9ddc595a02cf1baaab3e9595d77b0103c80d66bf | |
| parent | 5b0f516e7e1f6d2ea8ca0485ffe347a613b01a5c (diff) | |
Ajout du langage de tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
70 files changed, 1734 insertions, 904 deletions
@@ -32,6 +32,8 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \ kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/constant.cmi kernel/environ.cmi \ kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi library/global.cmi: kernel/constant.cmi kernel/environ.cmi \ @@ -47,13 +49,11 @@ library/library.cmi: lib/pp.cmi library/nametab.cmi: kernel/names.cmi library/redinfo.cmi: kernel/names.cmi kernel/term.cmi library/summary.cmi: kernel/names.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi proofs/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \ - pretyping/tacred.cmi kernel/term.cmi + kernel/term.cmi parsing/coqast.cmi: lib/dyn.cmi parsing/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ parsing/pcoq.cmi @@ -104,65 +104,70 @@ pretyping/syntax_def.cmi: kernel/names.cmi pretyping/rawterm.cmi pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi kernel/reduction.cmi kernel/term.cmi pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi -proofs/clenv.cmi: kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \ +proofs/clenv.cmi: kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ proofs/tacmach.cmi kernel/term.cmi lib/util.cmi proofs/evar_refiner.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ - proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi + proofs/proof_trees.cmi proofs/proof_type.cmi proofs/refiner.cmi \ + kernel/sign.cmi kernel/term.cmi proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ - lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi + lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi proofs/macros.cmi: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \ - proofs/proof_trees.cmi proofs/tacmach.cmi + proofs/proof_type.cmi proofs/tacmach.cmi proofs/pattern.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi proofs/pfedit.cmi: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ - kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi \ + kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi \ proofs/tacmach.cmi kernel/term.cmi proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/names.cmi lib/pp.cmi kernel/sign.cmi lib/stamps.cmi \ - kernel/term.cmi lib/util.cmi -proofs/refiner.cmi: lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi \ - kernel/term.cmi -proofs/tacinterp.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \ - proofs/proof_trees.cmi proofs/tacmach.cmi kernel/term.cmi + kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi \ + lib/stamps.cmi kernel/term.cmi lib/util.cmi +proofs/proof_type.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ + kernel/names.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \ + lib/util.cmi +proofs/refiner.cmi: lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + kernel/sign.cmi kernel/term.cmi +proofs/stock.cmi: kernel/names.cmi +proofs/tacinterp.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \ + lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi kernel/term.cmi proofs/tacmach.cmi: parsing/coqast.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi kernel/evd.cmi kernel/names.cmi lib/pp.cmi \ - proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \ - kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi + proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \ + proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi parsing/coqast.cmi \ - kernel/names.cmi proofs/pattern.cmi proofs/proof_trees.cmi \ + kernel/names.cmi proofs/pattern.cmi proofs/proof_type.cmi \ pretyping/rawterm.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ lib/util.cmi tactics/btermdn.cmi: kernel/generic.cmi proofs/pattern.cmi kernel/term.cmi tactics/dhyp.cmi: kernel/names.cmi proofs/tacmach.cmi -tactics/elim.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \ +tactics/elim.cmi: kernel/names.cmi proofs/proof_type.cmi proofs/tacmach.cmi \ tactics/tacticals.cmi kernel/term.cmi tactics/equality.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ tactics/hipattern.cmi kernel/names.cmi proofs/pattern.cmi \ - proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi \ + proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi \ tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ tactics/wcclausenv.cmi -tactics/hiddentac.cmi: kernel/names.cmi proofs/proof_trees.cmi \ +tactics/hiddentac.cmi: kernel/names.cmi proofs/proof_type.cmi \ tactics/tacentries.cmi proofs/tacmach.cmi kernel/term.cmi tactics/hipattern.cmi: kernel/evd.cmi kernel/names.cmi proofs/pattern.cmi \ - proofs/proof_trees.cmi kernel/sign.cmi tactics/stock.cmi kernel/term.cmi \ + proofs/proof_trees.cmi kernel/sign.cmi proofs/stock.cmi kernel/term.cmi \ lib/util.cmi tactics/inv.cmi: parsing/coqast.cmi kernel/names.cmi proofs/tacmach.cmi tactics/nbtermdn.cmi: tactics/btermdn.cmi kernel/generic.cmi \ proofs/pattern.cmi kernel/term.cmi tactics/stock.cmi: kernel/names.cmi -tactics/tacentries.cmi: proofs/proof_trees.cmi proofs/tacmach.cmi +tactics/tacentries.cmi: proofs/proof_type.cmi proofs/tacmach.cmi tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \ - proofs/pattern.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ + proofs/pattern.cmi proofs/proof_type.cmi kernel/reduction.cmi \ kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi tactics/tactics.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/environ.cmi \ - kernel/evd.cmi kernel/names.cmi proofs/proof_trees.cmi \ + kernel/evd.cmi kernel/names.cmi proofs/proof_type.cmi \ kernel/reduction.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ tactics/tacticals.cmi kernel/term.cmi tactics/tauto.cmi: proofs/tacmach.cmi kernel/term.cmi tactics/termdn.cmi: kernel/generic.cmi proofs/pattern.cmi kernel/term.cmi tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/names.cmi proofs/proof_trees.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi + kernel/names.cmi proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi \ + kernel/term.cmi toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi kernel/names.cmi \ pretyping/tacred.cmi kernel/term.cmi toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi @@ -177,11 +182,11 @@ toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi +toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \ toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ - proofs/proof_trees.cmi -toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi + proofs/proof_type.cmi config/coq_config.cmo: config/coq_config.cmi config/coq_config.cmx: config/coq_config.cmi dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi @@ -298,22 +303,30 @@ lib/dyn.cmo: lib/util.cmi lib/dyn.cmi lib/dyn.cmx: lib/util.cmx lib/dyn.cmi lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi -lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi -lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gmap.cmo: lib/gmap.cmi lib/gmap.cmx: lib/gmap.cmi +lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi +lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.cmi -lib/pp_control.cmo: lib/pp_control.cmi -lib/pp_control.cmx: lib/pp_control.cmi lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi +lib/pp_control.cmo: lib/pp_control.cmi +lib/pp_control.cmx: lib/pp_control.cmi lib/profile.cmo: lib/system.cmi lib/profile.cmi lib/profile.cmx: lib/system.cmx lib/profile.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi +lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/util.cmi library/declare.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi library/global.cmi library/impargs.cmi \ library/indrec.cmi kernel/inductive.cmi library/lib.cmi \ @@ -386,33 +399,25 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \ library/summary.cmi library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ library/summary.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi -lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi -lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/util.cmi parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \ kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \ kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/ast.cmi -parsing/astterm.cmo: parsing/ast.cmi kernel/closure.cmi parsing/coqast.cmi \ - library/declare.cmi kernel/environ.cmi pretyping/evarutil.cmi \ - kernel/evd.cmi kernel/generic.cmi library/global.cmi library/impargs.cmi \ - kernel/names.cmi library/nametab.cmi proofs/pattern.cmi parsing/pcoq.cmi \ - lib/pp.cmi pretyping/pretype_errors.cmi pretyping/pretyping.cmi \ - pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \ - pretyping/syntax_def.cmi pretyping/tacred.cmi kernel/term.cmi \ +parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ + kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \ + kernel/generic.cmi library/global.cmi library/impargs.cmi \ + kernel/names.cmi proofs/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \ + pretyping/pretype_errors.cmi pretyping/pretyping.cmi \ + pretyping/rawterm.cmi kernel/reduction.cmi pretyping/retyping.cmi \ + kernel/sign.cmi pretyping/syntax_def.cmi kernel/term.cmi \ pretyping/typing.cmi lib/util.cmi parsing/astterm.cmi -parsing/astterm.cmx: parsing/ast.cmx kernel/closure.cmx parsing/coqast.cmx \ - library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \ - kernel/evd.cmx kernel/generic.cmx library/global.cmx library/impargs.cmx \ - kernel/names.cmx library/nametab.cmx proofs/pattern.cmx parsing/pcoq.cmx \ - lib/pp.cmx pretyping/pretype_errors.cmx pretyping/pretyping.cmx \ - pretyping/rawterm.cmx kernel/reduction.cmx kernel/sign.cmx \ - pretyping/syntax_def.cmx pretyping/tacred.cmx kernel/term.cmx \ +parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \ + kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \ + kernel/generic.cmx library/global.cmx library/impargs.cmx \ + kernel/names.cmx proofs/pattern.cmx parsing/pcoq.cmx lib/pp.cmx \ + pretyping/pretype_errors.cmx pretyping/pretyping.cmx \ + pretyping/rawterm.cmx kernel/reduction.cmx pretyping/retyping.cmx \ + kernel/sign.cmx pretyping/syntax_def.cmx kernel/term.cmx \ pretyping/typing.cmx lib/util.cmx parsing/astterm.cmi parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi @@ -628,41 +633,43 @@ pretyping/typing.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ kernel/typeops.cmx lib/util.cmx pretyping/typing.cmi proofs/clenv.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ + parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \ kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi \ lib/util.cmi proofs/clenv.cmi proofs/clenv.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ + parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \ kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx \ lib/util.cmx proofs/clenv.cmi proofs/evar_refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ proofs/logic.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \ - kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi kernel/term.cmi \ - pretyping/typing.cmi lib/util.cmi proofs/evar_refiner.cmi + proofs/proof_type.cmi kernel/reduction.cmi proofs/refiner.cmi \ + lib/stamps.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + proofs/evar_refiner.cmi proofs/evar_refiner.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ proofs/logic.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \ - kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx kernel/term.cmx \ - pretyping/typing.cmx lib/util.cmx proofs/evar_refiner.cmi + proofs/proof_type.cmx kernel/reduction.cmx proofs/refiner.cmx \ + lib/stamps.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + proofs/evar_refiner.cmi proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ kernel/evd.cmi kernel/generic.cmi library/global.cmi kernel/names.cmi \ lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ - kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/type_errors.cmi kernel/typeops.cmi pretyping/typing.cmi \ - lib/util.cmi proofs/logic.cmi + proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi \ + pretyping/typing.cmi lib/util.cmi proofs/logic.cmi proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \ kernel/evd.cmx kernel/generic.cmx library/global.cmx kernel/names.cmx \ lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ - kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/type_errors.cmx kernel/typeops.cmx pretyping/typing.cmx \ - lib/util.cmx proofs/logic.cmi + proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \ + kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx \ + pretyping/typing.cmx lib/util.cmx proofs/logic.cmi proofs/macros.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ - parsing/pcoq.cmi lib/pp.cmi proofs/proof_trees.cmi library/summary.cmi \ + parsing/pcoq.cmi lib/pp.cmi proofs/proof_type.cmi library/summary.cmi \ kernel/term.cmi lib/util.cmi proofs/macros.cmi proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ library/libobject.cmx library/library.cmx kernel/names.cmx \ - parsing/pcoq.cmx lib/pp.cmx proofs/proof_trees.cmx library/summary.cmx \ + parsing/pcoq.cmx lib/pp.cmx proofs/proof_type.cmx library/summary.cmx \ kernel/term.cmx lib/util.cmx proofs/macros.cmi proofs/pattern.cmo: kernel/generic.cmi kernel/names.cmi pretyping/rawterm.cmi \ kernel/reduction.cmi kernel/term.cmi lib/util.cmi proofs/pattern.cmi @@ -672,54 +679,72 @@ proofs/pfedit.cmo: parsing/astterm.cmi kernel/constant.cmi \ library/declare.cmi lib/edit.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi library/global.cmi library/lib.cmi proofs/logic.cmi \ kernel/names.cmi lib/options.cmi lib/pp.cmi proofs/proof_trees.cmi \ - kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi \ - lib/util.cmi proofs/pfedit.cmi + proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ + pretyping/typing.cmi lib/util.cmi proofs/pfedit.cmi proofs/pfedit.cmx: parsing/astterm.cmx kernel/constant.cmx \ library/declare.cmx lib/edit.cmx kernel/environ.cmx kernel/evd.cmx \ kernel/generic.cmx library/global.cmx library/lib.cmx proofs/logic.cmx \ kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_trees.cmx \ - kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx \ - lib/util.cmx proofs/pfedit.cmi -proofs/proof_trees.cmo: parsing/ast.cmi parsing/coqast.cmi \ - pretyping/detyping.cmi kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ - lib/pp.cmi parsing/pretty.cmi parsing/printer.cmi kernel/sign.cmi \ - lib/stamps.cmi kernel/term.cmi parsing/termast.cmi pretyping/typing.cmi \ - lib/util.cmi proofs/proof_trees.cmi -proofs/proof_trees.cmx: parsing/ast.cmx parsing/coqast.cmx \ - pretyping/detyping.cmx kernel/environ.cmx kernel/evd.cmx kernel/names.cmx \ - lib/pp.cmx parsing/pretty.cmx parsing/printer.cmx kernel/sign.cmx \ - lib/stamps.cmx kernel/term.cmx parsing/termast.cmx pretyping/typing.cmx \ - lib/util.cmx proofs/proof_trees.cmi + proofs/proof_type.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \ + pretyping/typing.cmx lib/util.cmx proofs/pfedit.cmi +proofs/proof_trees.cmo: parsing/ast.cmi pretyping/detyping.cmi \ + kernel/environ.cmi kernel/evd.cmi kernel/names.cmi lib/pp.cmi \ + parsing/pretty.cmi parsing/printer.cmi proofs/proof_type.cmi \ + kernel/sign.cmi lib/stamps.cmi kernel/term.cmi parsing/termast.cmi \ + pretyping/typing.cmi lib/util.cmi proofs/proof_trees.cmi +proofs/proof_trees.cmx: parsing/ast.cmx pretyping/detyping.cmx \ + kernel/environ.cmx kernel/evd.cmx kernel/names.cmx lib/pp.cmx \ + parsing/pretty.cmx parsing/printer.cmx proofs/proof_type.cmx \ + kernel/sign.cmx lib/stamps.cmx kernel/term.cmx parsing/termast.cmx \ + pretyping/typing.cmx lib/util.cmx proofs/proof_trees.cmi +proofs/proof_type.cmo: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ + kernel/names.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \ + lib/util.cmi proofs/proof_type.cmi +proofs/proof_type.cmx: parsing/coqast.cmx kernel/environ.cmx kernel/evd.cmx \ + kernel/names.cmx lib/stamps.cmx pretyping/tacred.cmx kernel/term.cmx \ + lib/util.cmx proofs/proof_type.cmi proofs/refiner.cmo: parsing/ast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi kernel/instantiate.cmi proofs/logic.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ - kernel/sign.cmi lib/stamps.cmi kernel/term.cmi kernel/type_errors.cmi \ - lib/util.cmi proofs/refiner.cmi + parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \ + kernel/type_errors.cmi lib/util.cmi proofs/refiner.cmi proofs/refiner.cmx: parsing/ast.cmx kernel/environ.cmx kernel/evd.cmx \ kernel/generic.cmx kernel/instantiate.cmx proofs/logic.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ - kernel/sign.cmx lib/stamps.cmx kernel/term.cmx kernel/type_errors.cmx \ - lib/util.cmx proofs/refiner.cmi -proofs/tacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi proofs/macros.cmi \ - kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \ - kernel/term.cmi lib/util.cmi proofs/tacinterp.cmi -proofs/tacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx proofs/macros.cmx \ - kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/tacmach.cmx \ - kernel/term.cmx lib/util.cmx proofs/tacinterp.cmi + parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx kernel/term.cmx \ + kernel/type_errors.cmx lib/util.cmx proofs/refiner.cmi +proofs/stock.cmo: lib/bij.cmi lib/gmap.cmi lib/gmapl.cmi library/library.cmi \ + kernel/names.cmi lib/pp.cmi lib/util.cmi proofs/stock.cmi +proofs/stock.cmx: lib/bij.cmx lib/gmap.cmx lib/gmapl.cmx library/library.cmx \ + kernel/names.cmx lib/pp.cmx lib/util.cmx proofs/stock.cmi +proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \ + parsing/coqast.cmi kernel/environ.cmi kernel/generic.cmi lib/gmap.cmi \ + library/lib.cmi library/libobject.cmi proofs/macros.cmi kernel/names.cmi \ + library/nametab.cmi proofs/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi kernel/sign.cmi library/summary.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi kernel/term.cmi \ + pretyping/typing.cmi lib/util.cmi proofs/tacinterp.cmi +proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \ + parsing/coqast.cmx kernel/environ.cmx kernel/generic.cmx lib/gmap.cmx \ + library/lib.cmx library/libobject.cmx proofs/macros.cmx kernel/names.cmx \ + library/nametab.cmx proofs/pattern.cmx lib/pp.cmx proofs/proof_type.cmx \ + pretyping/rawterm.cmx kernel/sign.cmx library/summary.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx kernel/term.cmx \ + pretyping/typing.cmx lib/util.cmx proofs/tacinterp.cmi proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi library/declare.cmi \ kernel/environ.cmi proofs/evar_refiner.cmi kernel/evd.cmi \ kernel/generic.cmi kernel/instantiate.cmi proofs/logic.cmi \ kernel/names.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ - kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi lib/stamps.cmi \ - pretyping/tacred.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ - proofs/tacmach.cmi + proofs/proof_type.cmi kernel/reduction.cmi proofs/refiner.cmi \ + kernel/sign.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \ + pretyping/typing.cmi lib/util.cmi proofs/tacmach.cmi proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx library/declare.cmx \ kernel/environ.cmx proofs/evar_refiner.cmx kernel/evd.cmx \ kernel/generic.cmx kernel/instantiate.cmx proofs/logic.cmx \ kernel/names.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ - kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx \ - pretyping/tacred.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ - proofs/tacmach.cmi + proofs/proof_type.cmx kernel/reduction.cmx proofs/refiner.cmx \ + kernel/sign.cmx lib/stamps.cmx pretyping/tacred.cmx kernel/term.cmx \ + pretyping/typing.cmx lib/util.cmx proofs/tacmach.cmi scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \ @@ -728,7 +753,7 @@ tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \ tactics/hipattern.cmi kernel/inductive.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi proofs/logic.cmi \ kernel/names.cmi lib/options.cmi proofs/pattern.cmi proofs/pfedit.cmi \ - lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \ pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \ library/summary.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ @@ -740,7 +765,7 @@ tactics/auto.cmx: parsing/astterm.cmx tactics/btermdn.cmx proofs/clenv.cmx \ tactics/hipattern.cmx kernel/inductive.cmx library/lib.cmx \ library/libobject.cmx library/library.cmx proofs/logic.cmx \ kernel/names.cmx lib/options.cmx proofs/pattern.cmx proofs/pfedit.cmx \ - lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \ pretyping/rawterm.cmx kernel/reduction.cmx kernel/sign.cmx \ library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ @@ -754,7 +779,7 @@ tactics/dhyp.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \ parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ library/global.cmi library/lib.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi tactics/nbtermdn.cmi \ - proofs/pattern.cmi parsing/pcoq.cmi lib/pp.cmi proofs/proof_trees.cmi \ + proofs/pattern.cmi parsing/pcoq.cmi lib/pp.cmi proofs/proof_type.cmi \ pretyping/rawterm.cmi kernel/reduction.cmi library/summary.cmi \ proofs/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ tactics/tactics.cmi kernel/term.cmi lib/util.cmi \ @@ -763,7 +788,7 @@ tactics/dhyp.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \ parsing/coqast.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ library/global.cmx library/lib.cmx library/libobject.cmx \ library/library.cmx kernel/names.cmx tactics/nbtermdn.cmx \ - proofs/pattern.cmx parsing/pcoq.cmx lib/pp.cmx proofs/proof_trees.cmx \ + proofs/pattern.cmx parsing/pcoq.cmx lib/pp.cmx proofs/proof_type.cmx \ pretyping/rawterm.cmx kernel/reduction.cmx library/summary.cmx \ proofs/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx \ @@ -771,11 +796,11 @@ tactics/dhyp.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \ tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi tactics/elim.cmo: proofs/clenv.cmi kernel/generic.cmi tactics/hiddentac.cmi \ - tactics/hipattern.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \ + tactics/hipattern.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ kernel/reduction.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ tactics/tactics.cmi kernel/term.cmi lib/util.cmi tactics/elim.cmi tactics/elim.cmx: proofs/clenv.cmx kernel/generic.cmx tactics/hiddentac.cmx \ - tactics/hipattern.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \ + tactics/hipattern.cmx kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx \ kernel/reduction.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx tactics/elim.cmi tactics/equality.cmo: parsing/astterm.cmi parsing/coqast.cmi \ @@ -783,7 +808,7 @@ tactics/equality.cmo: parsing/astterm.cmi parsing/coqast.cmi \ lib/gmapl.cmi tactics/hipattern.cmi kernel/inductive.cmi \ kernel/instantiate.cmi library/lib.cmi library/libobject.cmi \ proofs/logic.cmi kernel/names.cmi proofs/pattern.cmi lib/pp.cmi \ - proofs/proof_trees.cmi kernel/reduction.cmi library/summary.cmi \ + proofs/proof_type.cmi kernel/reduction.cmi library/summary.cmi \ proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ kernel/typeops.cmi pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \ @@ -793,26 +818,26 @@ tactics/equality.cmx: parsing/astterm.cmx parsing/coqast.cmx \ lib/gmapl.cmx tactics/hipattern.cmx kernel/inductive.cmx \ kernel/instantiate.cmx library/lib.cmx library/libobject.cmx \ proofs/logic.cmx kernel/names.cmx proofs/pattern.cmx lib/pp.cmx \ - proofs/proof_trees.cmx kernel/reduction.cmx library/summary.cmx \ + proofs/proof_type.cmx kernel/reduction.cmx library/summary.cmx \ proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ kernel/typeops.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \ toplevel/vernacinterp.cmx tactics/wcclausenv.cmx tactics/equality.cmi -tactics/hiddentac.cmo: proofs/proof_trees.cmi tactics/tacentries.cmi \ +tactics/hiddentac.cmo: proofs/proof_type.cmi tactics/tacentries.cmi \ proofs/tacmach.cmi kernel/term.cmi tactics/hiddentac.cmi -tactics/hiddentac.cmx: proofs/proof_trees.cmx tactics/tacentries.cmx \ +tactics/hiddentac.cmx: proofs/proof_type.cmx tactics/tacentries.cmx \ proofs/tacmach.cmx kernel/term.cmx tactics/hiddentac.cmi tactics/hipattern.cmo: parsing/astterm.cmi proofs/clenv.cmi \ kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \ kernel/names.cmi proofs/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \ parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ - kernel/sosub.cmi tactics/stock.cmi kernel/term.cmi lib/util.cmi \ + kernel/sosub.cmi proofs/stock.cmi kernel/term.cmi lib/util.cmi \ tactics/hipattern.cmi tactics/hipattern.cmx: parsing/astterm.cmx proofs/clenv.cmx \ kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \ kernel/names.cmx proofs/pattern.cmx parsing/pcoq.cmx lib/pp.cmx \ parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ - kernel/sosub.cmx tactics/stock.cmx kernel/term.cmx lib/util.cmx \ + kernel/sosub.cmx proofs/stock.cmx kernel/term.cmx lib/util.cmx \ tactics/hipattern.cmi tactics/inv.cmo: tactics/auto.cmi proofs/clenv.cmi tactics/elim.cmi \ kernel/environ.cmi tactics/equality.cmi kernel/evd.cmi kernel/generic.cmi \ @@ -866,34 +891,32 @@ tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \ library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ library/global.cmi library/indrec.cmi kernel/inductive.cmi \ kernel/names.cmi proofs/pattern.cmi lib/pp.cmi parsing/pretty.cmi \ - proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \ - lib/stamps.cmi proofs/tacinterp.cmi proofs/tacmach.cmi kernel/term.cmi \ - parsing/termast.cmi lib/util.cmi tactics/wcclausenv.cmi \ - tactics/tacticals.cmi + kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi proofs/tacinterp.cmi \ + proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \ + tactics/wcclausenv.cmi tactics/tacticals.cmi tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \ library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ library/global.cmx library/indrec.cmx kernel/inductive.cmx \ kernel/names.cmx proofs/pattern.cmx lib/pp.cmx parsing/pretty.cmx \ - proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ - lib/stamps.cmx proofs/tacinterp.cmx proofs/tacmach.cmx kernel/term.cmx \ - parsing/termast.cmx lib/util.cmx tactics/wcclausenv.cmx \ - tactics/tacticals.cmi + kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \ + proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \ + tactics/wcclausenv.cmx tactics/tacticals.cmi tactics/tactics.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \ library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ library/global.cmi tactics/hipattern.cmi library/indrec.cmi \ kernel/inductive.cmi proofs/logic.cmi kernel/names.cmi proofs/pfedit.cmi \ - lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \ - lib/stamps.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ - pretyping/tacred.cmi tactics/tacticals.cmi kernel/term.cmi lib/util.cmi \ - tactics/tactics.cmi + lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi proofs/tacinterp.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ + kernel/term.cmi lib/util.cmi tactics/tactics.cmi tactics/tactics.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \ library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ library/global.cmx tactics/hipattern.cmx library/indrec.cmx \ kernel/inductive.cmx proofs/logic.cmx kernel/names.cmx proofs/pfedit.cmx \ - lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ - lib/stamps.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ - pretyping/tacred.cmx tactics/tacticals.cmx kernel/term.cmx lib/util.cmx \ - tactics/tactics.cmi + lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ + kernel/term.cmx lib/util.cmx tactics/tactics.cmi tactics/tauto.cmo: tactics/auto.cmi proofs/clenv.cmi library/declare.cmi \ kernel/environ.cmi kernel/generic.cmi tactics/hipattern.cmi \ kernel/names.cmi library/nametab.cmi proofs/pattern.cmi lib/pp.cmi \ @@ -1034,15 +1057,23 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \ toplevel/vernacinterp.cmx toplevel/toplevel.cmi toplevel/usage.cmo: toplevel/usage.cmi toplevel/usage.cmx: toplevel/usage.cmi +toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \ + lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \ + library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \ + lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \ + library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ pretyping/class.cmi toplevel/command.cmi parsing/coqast.cmi \ library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \ kernel/evd.cmi parsing/extend.cmi library/global.cmi library/goptions.cmi \ library/impargs.cmi library/lib.cmi library/libobject.cmi \ - library/library.cmi proofs/macros.cmi toplevel/metasyntax.cmi \ - kernel/names.cmi library/nametab.cmi lib/options.cmi parsing/pcoq.cmi \ - proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi toplevel/record.cmi \ + library/library.cmi toplevel/metasyntax.cmi kernel/names.cmi \ + library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \ + lib/pp_control.cmi parsing/pretty.cmi parsing/printer.cmi \ + proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \ kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi library/states.cmi \ lib/system.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ pretyping/tacred.cmi tactics/tactics.cmi kernel/term.cmi \ @@ -1053,31 +1084,23 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ library/declare.cmx toplevel/discharge.cmx kernel/environ.cmx \ kernel/evd.cmx parsing/extend.cmx library/global.cmx library/goptions.cmx \ library/impargs.cmx library/lib.cmx library/libobject.cmx \ - library/library.cmx proofs/macros.cmx toplevel/metasyntax.cmx \ - kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmx \ - proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx toplevel/record.cmx \ + library/library.cmx toplevel/metasyntax.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \ + lib/pp_control.cmx parsing/pretty.cmx parsing/printer.cmx \ + proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \ kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx library/states.cmx \ lib/system.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ pretyping/tacred.cmx tactics/tactics.cmx kernel/term.cmx \ kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ toplevel/vernacentries.cmi toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \ - toplevel/himsg.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ - proofs/proof_trees.cmi proofs/tacinterp.cmi lib/util.cmi \ + toplevel/himsg.cmi kernel/names.cmi lib/options.cmi proofs/pfedit.cmi \ + lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi lib/util.cmi \ toplevel/vernacinterp.cmi toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx lib/dyn.cmx \ - toplevel/himsg.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ - proofs/proof_trees.cmx proofs/tacinterp.cmx lib/util.cmx \ + toplevel/himsg.cmx kernel/names.cmx lib/options.cmx proofs/pfedit.cmx \ + lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \ toplevel/vernacinterp.cmi -toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \ - lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \ - library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \ - lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \ - library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - toplevel/vernac.cmi contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \ library/declare.cmi kernel/environ.cmi tactics/equality.cmi \ kernel/generic.cmi library/global.cmi kernel/inductive.cmi \ @@ -93,15 +93,15 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/astterm.cmo parsing/egrammar.cmo ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo -PROOFS=proofs/proof_trees.cmo proofs/logic.cmo \ +PROOFS=proofs/proof_type.cmo proofs/proof_trees.cmo proofs/logic.cmo \ proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ - proofs/macros.cmo proofs/tacinterp.cmo proofs/clenv.cmo \ - proofs/pfedit.cmo proofs/pattern.cmo + proofs/macros.cmo proofs/clenv.cmo proofs/stock.cmo proofs/pattern.cmo \ + proofs/tacinterp.cmo proofs/pfedit.cmo TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ - tactics/nbtermdn.cmo tactics/stock.cmo tactics/hipattern.cmo \ - tactics/wcclausenv.cmo tactics/tacticals.cmo tactics/tactics.cmo \ - tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo + tactics/nbtermdn.cmo tactics/hipattern.cmo tactics/wcclausenv.cmo \ + tactics/tacticals.cmo tactics/tactics.cmo tactics/tacentries.cmo \ + tactics/hiddentac.cmo tactics/elim.cmo TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ toplevel/metasyntax.cmo toplevel/command.cmo toplevel/record.cmo \ diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v index 1cbf284a55..67b7751b3f 100644 --- a/contrib/omega/Zcomplements.v +++ b/contrib/omega/Zcomplements.v @@ -70,9 +70,9 @@ Lemma Zlt_Zmult_right : (x,y,z:Z)`z>0` -> `x < y` -> `x*z < y*z`. Intros; Rewrite (Zs_pred z); Generalize (Zgt0_le_pred H); Intro; Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`; -[ Simpl; Do 2 (Rewrite Zmult_n_1); Assumption -| Unfold Zs; Intros x0 Hx0; Do 6 (Rewrite Zmult_plus_distr_r); - Repeat (Rewrite Zmult_n_1); +[ Simpl; Do 2 '(Rewrite Zmult_n_1); Assumption +| Unfold Zs; Intros x0 Hx0; Do 6 '(Rewrite Zmult_plus_distr_r); + Repeat Rewrite Zmult_n_1; Intro; Apply Zlt_Zplus; Assumption | Assumption ]. Save. @@ -82,7 +82,7 @@ Intros x y z H; Rewrite (Zs_pred z). Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`->`x < y`. Simpl; Do 2 Rewrite Zmult_n_1; Auto 1. Unfold Zs. -Intros x0 Hx0; Repeat (Rewrite Zmult_plus_distr_r). +Intros x0 Hx0; Repeat Rewrite Zmult_plus_distr_r. Repeat Rewrite Zmult_n_1. Omega. Unfold Zpred; Omega. diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index f57a17f30e..dd9b4b1e3a 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -11,7 +11,7 @@ open Util open Pp open Reduction -open Proof_trees +open Proof_type open Ast open Names open Generic diff --git a/kernel/environ.ml b/kernel/environ.ml index fdfc540d26..4471d5b873 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -103,10 +103,10 @@ let add_abstraction sp ab env = env_abstractions = new_abs; env_locals = new_locals } in { env with env_globals = new_globals } - -let new_meta = - let meta_ctr = ref 0 in - fun () -> (incr meta_ctr; !meta_ctr) + +let meta_ctr=ref 0;; + +let new_meta ()=incr meta_ctr;!meta_ctr;; (* Access functions. *) @@ -310,4 +310,3 @@ type unsafe_judgment = { let cast_of_judgment = function | { uj_val = DOP2 (Cast,_,_) as c } -> c | { uj_val = c; uj_type = ty } -> mkCast c ty - diff --git a/kernel/term.ml b/kernel/term.ml index a83a8c6f23..16d63fcbfc 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1307,6 +1307,21 @@ let rec occur_meta = function | DOP0(Meta(_)) -> true | _ -> false +(*Returns the maximum of metas. Returns -1 if there is no meta*) +(*let rec max_occur_meta=function + DOP2(Prod,t,DLAM(_,c)) -> + max (max_occur_meta t) (max_occur_meta c) + |DOP2(Lambda,t,DLAM(_,c)) -> + max (max_occur_meta t) (max_occur_meta c) + |DOPN(_,cl) -> + (try + List.hd (Sort.list (>) (List.map max_occur_meta (Array.to_list cl))) + with + Failure "hd" -> -1) + |DOP2(Cast,c,t) -> max (max_occur_meta c) (max_occur_meta t) + |DOP0(Meta n) -> n + |_ -> -1;;*) + let rel_vect = (Generic.rel_vect : int -> int -> constr array) let occur_existential = @@ -1584,3 +1599,54 @@ let sub_term_with_unif cref ceq= None else Some ((subst_with_lmeta l ceq),nb) + +let constr_display csr= + let rec term_display=function + DOP0(a) -> "DOP0("^(oper_display a)^")" + |DOP1(a,b) -> "DOP1("^(oper_display a)^","^(term_display b)^")" + |DOP2(a,b,c) -> + "DOP2("^(oper_display a)^","^(term_display b)^","^(term_display c)^")" + |DOPN(a,b) -> + "DOPN("^(oper_display a)^",[|"^(Array.fold_right (fun x i -> + (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|])" + |DOPL(a,b) -> + "DOPL("^(oper_display a)^",[|"^(List.fold_right (fun x i -> + (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|]" + |DLAM(a,b) -> "DLAM("^(name_display a)^","^(term_display b)^")" + |DLAMV(a,b) -> + "DLAMV("^(name_display a)^",[|"^(Array.fold_right (fun x i -> + (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|]" + |VAR(a) -> "VAR "^(string_of_id a) + |Rel(a) -> "Rel "^(string_of_int a) + and oper_display=function + Meta(a) -> "?"^(string_of_int a) +(* |XTRA(a,_) -> "XTRA("^a^",[ast])"*) + |Sort(a) -> "Sort("^(sort_display a)^")" +(* |Implicit -> "Implicit"*) + |Cast -> "Cast" + |Prod -> "Prod" + |Lambda -> "Lambda" + |AppL -> "AppL" + |Const(sp) -> "Const("^(string_of_path sp)^")" + |Abst(sp) -> "Abst("^(string_of_path sp)^")" + |MutInd(sp,i) -> "MutInd("^(string_of_path sp)^","^(string_of_int i)^")" + |MutConstruct((sp,i),j) -> + "MutConstruct(("^(string_of_path sp)^","^(string_of_int i)^"),"^ + (string_of_int j)^")" +(* |MutCase(ci) -> "MutCase("^(ci_display ci)^")"*) + |Fix(t,i) -> + "Fix([|"^(Array.fold_right (fun x i -> (string_of_int x)^(if not(i="") + then (";"^i) else "")) t "")^"|],"^(string_of_int i)^")" + |CoFix(i) -> "CoFix "^(string_of_int i) + and sort_display=function + Prop(Pos) -> "Prop(Pos)" + |Prop(Null) -> "Prop(Null)" + |Type(_) -> "Type" +(* and ci_display=function + Some(sp,i) -> "Some("^(string_of_path sp)^","^(string_of_int i)^")" + |None -> "None"*) + and name_display=function + Name(id) -> "Name("^(string_of_id id)^")" + |Anonymous -> "Anonymous" + in + mSG [<'sTR (term_display csr);'fNL>];; diff --git a/kernel/term.mli b/kernel/term.mli index dc9684b923..145546b55c 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -514,6 +514,10 @@ val sort_hdchar : sorts -> string (*s Occur check functions. *) val occur_meta : constr -> bool + +(*Returns the maximum of metas. Returns -1 if there is no meta*) +(*val max_occur_meta:constr->int;;*) + val occur_existential : constr -> bool val rel_vect : int -> int -> constr array @@ -557,3 +561,5 @@ val hcons_constr: (typed_type -> typed_type) val hcons1_constr : constr -> constr + +val constr_display: constr -> unit;; diff --git a/lib/util.ml b/lib/util.ml index 963ed51930..cc2f514a40 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -130,7 +130,7 @@ let list_map2_i f i l1 l2 = let list_index x = let rec index_x n = function | y::l -> if x = y then n else index_x (succ n) l - | [] -> failwith "index" + | [] -> raise Not_found in index_x 1 diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 533856fc12..4bef9a0eb9 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -250,9 +250,13 @@ let check_capture s ty = function [< 'sTR ("The variable "^s^" occurs in its type") >] | _ -> () -let dbize k allow_soapp sigma = +let dbize k sigma env allow_soapp lvar = let rec dbrec env = function - | Nvar(loc,s) -> fst (dbize_ref k sigma env loc s) + | Nvar(loc,s) -> + if List.mem s lvar then + RRef(loc,RVar (id_of_string s)) + else + fst (dbize_ref k sigma env loc s) (* | Slam(_,ona,Node(_,"V$",l)) -> @@ -306,8 +310,13 @@ let dbize k allow_soapp sigma = | Node(loc,"APPLISTEXPL", f::args) -> RApp (loc,dbrec env f,List.map (dbrec env) args) | Node(loc,"APPLIST", Nvar(locs,s)::args) -> - let (c, impargs) = dbize_ref k sigma env locs s in - RApp (loc, c, dbize_args env impargs args) + let (c, impargs) = + if List.mem s lvar then + RRef(loc,RVar (id_of_string s)),[] + else + dbize_ref k sigma env locs s + in + RApp (loc, c, dbize_args env impargs args) | Node(loc,"APPLIST", f::args) -> RApp (loc,dbrec env f,List.map (dbrec env) args) @@ -403,13 +412,28 @@ let dbize k allow_soapp sigma = aux 1 l args in - dbrec + dbrec env (* constr_of_com takes an environment of typing assumptions, * and translates a command to a constr. *) +(*Takes a list of variables which must not be globalized*) +let interp_rawconstr_gen sigma env allow_soapp lvar com = + dbize CCI sigma (unitize_env (context env)) allow_soapp lvar com + let interp_rawconstr sigma env com = - dbize CCI false sigma (unitize_env (context env)) com + interp_rawconstr_gen sigma env false [] com + +(*The same as interp_rawconstr but with a list of variables which must not be + globalized*) +let interp_rawconstr_wo_glob sigma env lvar com = + dbize CCI sigma (unitize_env (context env)) false lvar com + +(*let raw_fconstr_of_com sigma env com = + dbize_fw sigma (unitize_env (context env)) [] com + +let raw_constr_of_compattern sigma env com = + dbize_cci sigma (unitize_env env) com*) (* Globalization of AST quotations (mainly used in command quotations to get statically bound idents in grammar or pretty-printing rules) *) @@ -501,14 +525,29 @@ let interp_constr_gen is_ass sigma env com = let interp_constr sigma env c = interp_constr_gen false sigma env c let interp_type sigma env c = interp_constr_gen true sigma env c - let judgment_of_com sigma env com = let c = interp_rawconstr sigma env com in try - ise_resolve false sigma [] env c + ise_resolve false sigma [] env [] [] c with e -> Stdpp.raise_with_loc (Ast.loc com) e +(*To retype a list of key*constr with undefined key*) +let retype_list sigma env lst= + List.map (fun (x,csr) -> (x,Retyping.mk_unsafe_judgment env sigma csr)) lst;; + +(*Interprets a constr according to two lists of instantiations (variables and + metas)*) +let interp_constr1 sigma env lvar lmeta com = + let c = + interp_rawconstr_gen sigma env false (List.map (fun x -> string_of_id (fst + x)) lvar) com + and rtype=fun lst -> retype_list sigma env lst in + try + ise_resolve2 sigma env (rtype lvar) (rtype lmeta) c + with e -> + Stdpp.raise_with_loc (Ast.loc com) e;; + let typed_type_of_com sigma env com = let c = interp_rawconstr sigma env com in try @@ -521,6 +560,15 @@ let typed_type_of_com sigma env com = let interp_casted_constr sigma env com typ = ise_resolve_casted sigma env typ (interp_rawconstr sigma env com) +(*Interprets a casted constr according to two lists of instantiations + (variables and metas)*) +let interp_casted_constr1 sigma env lvar lmeta com typ = + let c = + interp_rawconstr_gen sigma env false (List.map (fun x -> string_of_id (fst + x)) lvar) com + and rtype=fun lst -> retype_list sigma env lst in + ise_resolve_casted_gen sigma env (rtype lvar) (rtype lmeta) typ c;; + (* let dbize_fw sigma env com = dbize FW sigma env com @@ -619,101 +667,9 @@ let pattern_of_rawconstr c = (!metas,p) let interp_constrpattern sigma env com = - let c = dbize CCI true sigma (unitize_env (context env)) com in + let c = dbize CCI sigma (unitize_env (context env)) true [] com in try pattern_of_rawconstr c with e -> Stdpp.raise_with_loc (Ast.loc com) e -(* Translation of reduction expression: we need trad because of Fold - * Moreover, reduction expressions are used both in tactics and in - * vernac. *) - -open Closure -open Tacred - -let glob_nvar com = - let s = nvar_of_ast com in - try - Nametab.sp_of_id CCI (id_of_string s) - with Not_found -> - error ("unbound variable "^s) - -let cvt_pattern sigma env = function - | Node(_,"PATTERN", Node(_,"COMMAND",[com])::nums) -> - let occs = List.map num_of_ast nums in - let c = interp_constr sigma env com in - let j = Typing.unsafe_machine env sigma c in - (occs, j.uj_val, j.uj_type) - | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern") - -let cvt_unfold = function - | Node(_,"UNFOLD", com::nums) -> (List.map num_of_ast nums, glob_nvar com) - | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold") - -let cvt_fold sigma sign = function - | Node(_,"COMMAND",[c]) -> interp_constr sigma sign c - | arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold") - -let flag_of_ast lf = - let beta = ref false in - let delta = ref false in - let iota = ref false in - let idents = ref (None: (sorts oper -> bool) option) in - let set_flag = function - | Node(_,"Beta",[]) -> beta := true - | Node(_,"Delta",[]) -> delta := true - | Node(_,"Iota",[]) -> iota := true - | Node(loc,"Unf",l) -> - if !delta then - if !idents = None then - let idl = List.map glob_nvar l in - idents := Some - (function - | Const sp -> List.mem sp idl - | Abst sp -> List.mem sp idl - | _ -> false) - else - user_err_loc - (loc,"flag_of_ast", - [< 'sTR"Cannot specify identifiers to unfold twice" >]) - else - user_err_loc(loc,"flag_of_ast", - [< 'sTR"Delta must be specified before" >]) - | Node(loc,"UnfBut",l) -> - if !delta then - if !idents = None then - let idl = List.map glob_nvar l in - idents := Some - (function - | Const sp -> not (List.mem sp idl) - | Abst sp -> not (List.mem sp idl) - | _ -> false) - else - user_err_loc - (loc,"flag_of_ast", - [< 'sTR"Cannot specify identifiers to unfold twice" >]) - else - user_err_loc(loc,"flag_of_ast", - [< 'sTR"Delta must be specified before" >]) - | arg -> invalid_arg_loc (Ast.loc arg,"flag_of_ast") - in - List.iter set_flag lf; - { r_beta = !beta; - r_iota = !iota; - r_delta = match (!delta,!idents) with - | (false,_) -> (fun _ -> false) - | (true,None) -> (fun _ -> true) - | (true,Some p) -> p } - -let redexp_of_ast sigma sign = function - | ("Red", []) -> Red - | ("Hnf", []) -> Hnf - | ("Simpl", []) -> Simpl - | ("Unfold", ul) -> Unfold (List.map cvt_unfold ul) - | ("Fold", cl) -> Fold (List.map (cvt_fold sigma sign) cl) - | ("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast lf) - | ("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast lf) - | ("Pattern",lp) -> Pattern (List.map (cvt_pattern sigma sign) lp) - | (s,_) -> invalid_arg ("malformed reduction-expression: "^s) - diff --git a/parsing/astterm.mli b/parsing/astterm.mli index 1383dc655f..46c8f5b665 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -20,12 +20,21 @@ val interp_type : 'a evar_map -> env -> Coqast.t -> constr val typed_type_of_com : 'a evar_map -> env -> Coqast.t -> typed_type val judgment_of_com : 'a evar_map -> env -> Coqast.t -> unsafe_judgment +(*Interprets a constr according to two lists of instantiations (variables and + metas)*) +val interp_constr1 : + 'a evar_map -> env -> (identifier * constr) list -> + (int * constr) list -> Coqast.t -> constr + +(*Interprets a casted constr according to two lists of instantiations + (variables and metas)*) +val interp_casted_constr1 : + 'a evar_map -> env -> (identifier * constr) list -> + (int * constr) list -> Coqast.t -> constr -> constr + val interp_constrpattern : 'a evar_map -> env -> Coqast.t -> int list * constr_pattern -val redexp_of_ast : - 'a evar_map -> env -> string * Coqast.t list -> Tacred.red_expr - (* Translation rules from V6 to V7: constr_of_com_casted -> interp_casted_constr diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index dec8594750..41f0a82d4b 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -42,7 +42,7 @@ GEXTEND Gram [ [ c = Constr.sort -> <:ast< (CONSTR $c) >> ] ] ; tacarg: - [ [ tcl = Tactic.tactic_com_list -> tcl ] ] + [ [ tcl = Tactic.tactic -> tcl ] ] ; END; diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 4ab8b33ac2..96be64616d 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -16,7 +16,9 @@ GEXTEND Gram [ [ c = Prim.ast -> c ] ] ; constr: - [ [ c = constr8 -> c ] ] + [ [ c = constr8 -> c + | IDENT "Eval"; rtc=Tactic.red_tactic; "in"; c=constr8 -> + <:ast<(EVAL $c (REDEXP $rtc))>> ] ] ; lconstr: [ [ c = constr10 -> c ] ] diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index f19e373733..9a64fd03c1 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -16,9 +16,15 @@ GEXTEND Gram identarg: [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ] ; + pure_numarg: + [ [ n = Prim.number -> n + | "-"; n = Prim.number -> Coqast.Num (Ast.loc n, ( - Ast.num_of_ast n)) + ] ] + ; numarg: [ [ n = Prim.number -> n | "-"; n = Prim.number -> Coqast.Num (Ast.loc n, ( - Ast.num_of_ast n)) + | id = identarg -> id ] ] ; constrarg: @@ -27,6 +33,9 @@ GEXTEND Gram lconstrarg: [ [ c = Constr.lconstr -> <:ast< (COMMAND $c) >> ] ] ; + castedconstrarg: + [ [ c = Constr.constr -> <:ast< (CASTEDCOMMAND $c) >> ] ] + ; ne_identarg_list: [ [ l = LIST1 identarg -> l ] ] ; @@ -34,15 +43,18 @@ GEXTEND Gram [ [ n = numarg; l = ne_num_list -> n :: l | n = numarg -> [n] ] ] ; pattern_occ: - [ [ nl = ne_num_list; c = constrarg -> <:ast< (PATTERN $c ($LIST $nl)) >> + [ [ nl = LIST1 pure_numarg; c = constrarg -> + <:ast< (PATTERN $c ($LIST $nl)) >> | c = constrarg -> <:ast< (PATTERN $c) >> ] ] ; ne_pattern_list: [ [ l = LIST1 pattern_occ -> l ] ] ; pattern_occ_hyp: - [ [ nl = ne_num_list; IDENT "Goal" -> <:ast<(CCLPATTERN ($LIST $nl))>> - | nl = ne_num_list; id = identarg -> <:ast<(HYPPATTERN $id ($LIST $nl))>> + [ [ nl = LIST1 pure_numarg; IDENT "Goal" -> + <:ast<(CCLPATTERN ($LIST $nl))>> + | nl = LIST1 pure_numarg; id = identarg -> + <:ast<(HYPPATTERN $id ($LIST $nl))>> | IDENT "Goal" -> <:ast< (CCLPATTERN) >> | id = identarg -> <:ast< (HYPPATTERN $id) >> ] ] ; @@ -53,8 +65,8 @@ GEXTEND Gram [ [ p= ne_intropattern -> <:ast< (INTROPATTERN $p)>> ]] ; ne_intropattern: - [ [ tc = LIST1 simple_intropattern -> - <:ast< (LISTPATTERN ($LIST $tc))>> ] ] + [ [ tc = LIST1 simple_intropattern -> + <:ast< (LISTPATTERN ($LIST $tc))>> ] ] ; simple_intropattern: [ [ "["; tc = LIST1 intropattern SEP "|" ; "]" -> @@ -86,7 +98,7 @@ GEXTEND Gram | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var "c1" c | _ -> assert false in <:ast<(BINDINGS (BINDING ($VAR $id) $c2) ($LIST $bl))>> - | n = numarg; ":="; c = constrarg; bl = simple_binding_list -> + | n = pure_numarg; ":="; c = constrarg; bl = simple_binding_list -> <:ast<(BINDINGS (BINDING $n $c) ($LIST $bl))>> | c1 = constrarg; bl = com_binding_list -> <:ast<(BINDINGS (BINDING $c1) ($LIST $bl))>> @@ -105,7 +117,8 @@ GEXTEND Gram [ [ c = constrarg; l = constrarg_list -> c :: l | -> [] ] ] ; unfold_occ: - [ [ nl = ne_num_list; c = identarg -> <:ast< (UNFOLD $c ($LIST $nl)) >> + [ [ nl = LIST1 pure_numarg; c = identarg -> + <:ast< (UNFOLD $c ($LIST $nl)) >> | c = identarg -> <:ast< (UNFOLD $c) >> ] ] ; ne_unfold_occ_list: @@ -169,20 +182,83 @@ GEXTEND Gram (* Tactics grammar rules *) GEXTEND Gram - tactic_com_list: - [ [ y = tactic_com; ";"; l = LIST1 tactic_com_tail SEP ";" -> - <:ast< (TACTICLIST $y ($LIST $l)) >> - | y = tactic_com -> <:ast< (TACTICLIST $y) >> ] ] - ; - tactic_com_tail: - [ [ t1 = tactic_com -> t1 - | "["; l = LIST0 tactic_com_list SEP "|"; "]" -> - <:ast< (TACLIST ($LIST $l)) >> ] ] - ; - tactic_com: - [ [ st = simple_tactic; "Orelse"; tc = tactic_com -> - <:ast< (ORELSE $st $tc) >> - | st = simple_tactic -> st ] ] + input_fun: + [ [ l = identarg -> l + | "()" -> <:ast< (VOID) >> ] ] + ; + let_clause: + [ [ id = identarg; "="; te=tactic_expr -> <:ast< (LETCLAUSE $id $te) >> ] ] + ; + rec_clause: + [ [ name = identarg; it = LIST1 input_fun; "->"; body = tactic_expr -> + <:ast< (RECCLAUSE $name (FUNVAR ($LIST $it)) $body) >> ] ] + ; + match_hyps: + [ [ id = identarg; ":"; pc = constrarg -> + <:ast< (MATCHCONTEXTHYPS $id $pc) >> + | IDENT "_"; ":"; pc = constrarg -> <:ast< (MATCHCONTEXTHYPS $pc) >> ] ] + ; + match_context_rule: + [ [ "["; largs = LIST0 match_hyps SEP ";"; "|-"; pc = constrarg; "]"; "->"; + te = tactic_expr -> + <:ast< (MATCHCONTEXTRULE ($LIST $largs) $pc $te) >> + | IDENT "_"; "->"; te = tactic_expr -> <:ast< (MATCHCONTEXTRULE $te) >> + ] ] + ; + match_rule: + [ [ "["; com = constrarg; "]"; "->"; te = tactic_expr -> + <:ast<(MATCHRULE $com $te)>> + | IDENT "_"; "->"; te = tactic_expr -> <:ast< (MATCHRULE $te) >> ] ] + ; + tactic_expr: + [ [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> + <:ast< (TACTICLIST $ta0 $ta1) >> + | ta = tactic_expr; ";"; "["; lta = LIST0 tactic_expr SEP "|"; "]" -> + <:ast< (TACTICLIST $ta (TACLIST ($LIST $lta))) >> + | y = tactic_atom -> y ] ] + ; + tactic_atom: + [ [ IDENT "Fun"; it = LIST1 input_fun ; "->"; body = tactic_expr -> + <:ast< (FUN (FUNVAR ($LIST $it)) $body) >> + | IDENT "Rec"; rc = rec_clause -> <:ast< (REC $rc) >> + | IDENT "Rec"; rc = rec_clause; IDENT "In"; body = tactic_expr -> + <:ast< (REC (RECDECL $rc) $body) >> + | IDENT "Rec"; rc = rec_clause; IDENT "And"; + rcl = LIST1 rec_clause SEP IDENT "And"; IDENT "In"; + body = tactic_expr -> + <:ast< (REC (RECDECL $rc ($LIST $rcl)) $body) >> + | IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And"; IDENT "In"; + u = tactic_expr -> <:ast< (LET (LETDECL ($LIST $llc)) $u) >> + | IDENT "Match"; IDENT "Context"; IDENT "With"; + mrl = LIST1 match_context_rule SEP "|" -> + <:ast< (MATCHCONTEXT ($LIST $mrl)) >> + | IDENT "Match"; com = constrarg; IDENT "With"; + mrl = LIST1 match_rule SEP "|" -> <:ast< (MATCH $com ($LIST $mrl)) >> + | "'("; te = tactic_expr; ")" -> te + | "'("; te = tactic_expr; tel=LIST1 tactic_expr; ")" -> + <:ast< (APP $te ($LIST tel)) >> + | IDENT "First" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + <:ast<(FIRST ($LIST $l))>> + | IDENT "Info"; tc = tactic_expr -> <:ast< (INFO $tc) >> + | IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + <:ast<(TCLSOLVE ($LIST $l))>> + | IDENT "Try"; ta = tactic_atom -> <:ast< (TRY $ta) >> + | IDENT "Do"; n = numarg; ta = tactic_atom -> <:ast< (DO $n $ta) >> + | IDENT "Repeat"; ta = tactic_atom -> <:ast< (REPEAT $ta) >> + | IDENT "Idtac" -> <:ast< (IDTAC) >> + | IDENT "Fail" -> <:ast<(FAIL)>> + | ta0 = tactic_atom; "Orelse"; ta1 = tactic_atom -> + <:ast< (ORELSE $ta0 $ta1) >> + | st = simple_tactic -> st + | tca = tactic_arg -> tca ] ] + ; + tactic_arg: + [ [ "()" -> <:ast< (VOID) >> + | n = pure_numarg -> n + | c=constrarg -> + (match c with + Coqast.Node(_,"COMMAND",[Coqast.Nvar(_,s)]) -> <:ast<($VAR $s)>> + |_ -> c) ] ] ; simple_tactic: [ [ IDENT "Fix"; n = numarg -> <:ast< (Fix $n) >> @@ -224,8 +300,9 @@ GEXTEND Gram <:ast< (SuperAuto $a0 $a1 $a2 $a3) >> | IDENT "Auto"; n = numarg; IDENT "Decomp" -> <:ast< (DAuto $n) >> | IDENT "Auto"; IDENT "Decomp" -> <:ast< (DAuto) >> - | IDENT "Auto"; n = numarg; IDENT "Decomp"; p = numarg-> <:ast< (DAuto $n $p) >> - ]]; + | IDENT "Auto"; n = numarg; IDENT "Decomp"; p = numarg -> + <:ast< (DAuto $n $p) >> + ] ]; END GEXTEND Gram @@ -250,7 +327,7 @@ GEXTEND Gram <:ast< (Elim ($LIST $cl)) >> | IDENT "Assumption" -> <:ast< (Assumption) >> | IDENT "Contradiction" -> <:ast< (Contradiction) >> - | IDENT "Exact"; c = constrarg -> <:ast< (Exact $c) >> + | IDENT "Exact"; c = castedconstrarg -> <:ast< (Exact $c) >> | IDENT "OldElim"; c = constrarg -> <:ast< (OldElim $c) >> | IDENT "ElimType"; c = constrarg -> <:ast< (ElimType $c) >> | IDENT "Case"; cl = constrarg_binding_list -> @@ -264,10 +341,6 @@ GEXTEND Gram <:ast< (DecomposeOr $c) >> | IDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = constrarg -> <:ast< (DecomposeThese (CLAUSE ($LIST $l)) $c) >> - | IDENT "First" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" -> - <:ast<(FIRST ($LIST $l))>> - | IDENT "Solve" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" -> - <:ast<(TCLSOLVE ($LIST $l))>> | IDENT "Cut"; c = constrarg -> <:ast< (Cut $c) >> | IDENT "Specialize"; n = numarg; lcb = constrarg_binding_list -> <:ast< (Specialize $n ($LIST $lcb))>> @@ -285,13 +358,11 @@ GEXTEND Gram <:ast< (Clear (CLAUSE ($LIST $l))) >> | IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg -> <:ast< (MoveDep $id1 $id2) >> - | IDENT "Do"; n = numarg; tc = tactic_com -> <:ast< (DO $n $tc) >> - | IDENT "Try"; tc = tactic_com -> <:ast< (TRY $tc) >> - | IDENT "Info"; tc = tactic_com -> <:ast< (INFO $tc) >> - | IDENT "Repeat"; tc = tactic_com -> <:ast< (REPEAT $tc) >> - | IDENT "Abstract"; tc = tactic_com -> <:ast< (ABSTRACT (TACTIC $tc)) >> - | IDENT "Abstract"; tc = tactic_com; "using"; s=identarg - -> <:ast< (ABSTRACT $s (TACTIC $tc)) >> +(*To do: put Abstract in Refiner*) + | IDENT "Abstract"; tc = tactic_expr -> <:ast< (ABSTRACT (TACTIC $tc)) >> + | IDENT "Abstract"; tc = tactic_expr; "using"; s=identarg -> + <:ast< (ABSTRACT $s (TACTIC $tc)) >> +(*End of To do*) | IDENT "Left"; bl = with_binding_list -> <:ast< (Left $bl) >> | IDENT "Right"; bl = with_binding_list -> <:ast< (Right $bl) >> | IDENT "Split"; bl = with_binding_list -> <:ast< (Split $bl) >> @@ -305,23 +376,22 @@ GEXTEND Gram | IDENT "Absurd"; c = constrarg -> <:ast< (Absurd $c) >> | IDENT "Idtac" -> <:ast< (Idtac) >> | IDENT "Fail" -> <:ast< (Fail) >> - | "("; tcl = tactic_com_list; ")" -> tcl | r = red_tactic; cl = clausearg -> <:ast< (Reduce (REDEXP $r) $cl) >> (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *) | IDENT "Change"; c = constrarg; cl = clausearg -> <:ast< (Change $c $cl) >> | IDENT "ML"; s = Prim.string -> <:ast< (MLTACTIC $s) >> ] - | [ id = identarg; l = constrarg_list -> +(* | [ id = identarg; l = constrarg_list -> match (isMeta (nvar_of_ast id), l) with | (true, []) -> id | (false, _) -> <:ast< (CALL $id ($LIST $l)) >> | _ -> Util.user_err_loc (loc, "G_tactic.meta_tactic", [< 'sTR"Cannot apply arguments to a meta-tactic." >]) - ] ] + ] *)] ; tactic: - [ [ tac = tactic_com_list -> tac ] ] + [ [ tac = tactic_expr -> tac ] ] ; END diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 25010016ca..bea4c46aa5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -2,7 +2,9 @@ (* $Id$ *) open Pcoq - +open Pp +open Tactic +open Util open Vernac GEXTEND Gram @@ -121,7 +123,8 @@ GEXTEND Gram [ [ IDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]"; ":="; c = constrarg; "." -> <:ast< (ABSTRACTION $id $c ($LIST $l)) >> - ] ]; + ] ] + ; END (* Gallina inductive declarations *) @@ -425,6 +428,10 @@ GEXTEND Gram [ [ -> [] | ":"; l = LIST1 identarg -> l ] ] ; + vrec_clause: + [ [ name=identarg; it=LIST1 input_fun; ":="; body=tactic_expr -> + <:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ] + ; command: [ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >> | IDENT "Goal"; "." -> <:ast< (GOAL) >> @@ -481,11 +488,29 @@ GEXTEND Gram (* Tactic Definition *) - | IDENT "Tactic"; "Definition"; id = identarg; "["; - ids = ne_identarg_list; "]"; ":="; tac = Prim.astact; "." -> - <:ast< (TacticDefinition $id (AST $tac) ($LIST $ids)) >> - | IDENT "Tactic"; "Definition"; id = identarg; ":="; tac = Prim.astact; - "." -> <:ast< (TacticDefinition $id (AST $tac)) >> + |IDENT "Tactic"; "Definition"; name=identarg; ":="; body=Tactic.tactic; + "." -> <:ast<(TACDEF $name (AST $body))>> + |IDENT "Tactic"; "Definition"; name=identarg; largs=LIST1 input_fun; + ":="; body=Tactic.tactic; "." -> + <:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>> + |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause ; "." -> + (match vc with + Coqast.Node(_,"RECCLAUSE",nme::tl) -> + <:ast<(TACDEF $nme (AST (REC $vc)))>> + |_ -> + anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">]) + |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause; + IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." -> + let nvcl= + List.fold_right + (fun e b -> match e with + Coqast.Node(_,"RECCLAUSE",nme::_) -> + nme::<:ast<(AST (REC $e))>>::b + |_ -> + anomalylabstrm "Gram.vernac" [<'sTR + "Not a correct RECCLAUSE">]) (vc::vcl) [] + in + <:ast<(TACDEF ($LIST $nvcl))>> (* Hints for Auto and EAuto *) diff --git a/parsing/lexer.mll b/parsing/lexer.mll index 847b9a8fae..dca9a2fdd7 100644 --- a/parsing/lexer.mll +++ b/parsing/lexer.mll @@ -135,7 +135,8 @@ rule token = parse if is_keyword s then ("",s) else ("IDENT",s) } | decimal_literal | hex_literal | oct_literal | bin_literal { ("INT", Lexing.lexeme lexbuf) } - | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";" | "`" | "->" + | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";"| "`" | "()" | "'(" + | "->" { ("", Lexing.lexeme lexbuf) } | symbolchar+ { ("", Lexing.lexeme lexbuf) } diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 418188be5f..f0b13f23e6 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -272,6 +272,7 @@ module Tactic = Hashtbl.add utactic s (ListAst e); e let binding_list = gec "binding_list" + let castedconstrarg = gec "castedconstrarg" let com_binding_list = gec_list "com_binding_list" let constrarg = gec "constrarg" let constrarg_binding_list = gec_list "constrarg_binding_list" @@ -279,8 +280,13 @@ module Tactic = let lconstrarg_binding_list = gec_list "lconstrarg_binding_list" let constrarg_list = gec_list "constrarg_list" let identarg = gec "identarg" + let input_fun = gec "input_fun" let lconstrarg = gec "lconstrarg" + let let_clause = gec "let_clause" let clausearg = gec "clausearg" + let match_context_rule = gec "match_context_rule" + let match_hyps = gec "match_hyps" + let match_rule = gec "match_rule" let ne_identarg_list = gec_list "ne_identarg_list" let ne_num_list = gec_list "ne_num_list" let ne_pattern_list = gec_list "ne_pattern_list" @@ -290,6 +296,7 @@ module Tactic = let ne_intropattern = gec "ne_intropattern" let simple_intropattern = gec "simple_intropattern" let ne_unfold_occ_list = gec_list "ne_unfold_occ_list" + let rec_clause = gec "rec_clause" let red_tactic = gec "red_tactic" let red_flag = gec "red_flag" let autoarg_depth = gec "autoarg_depth" @@ -300,13 +307,14 @@ module Tactic = let numarg = gec "numarg" let pattern_occ = gec "pattern_occ" let pattern_occ_hyp = gec "pattern_occ_hyp" + let pure_numarg = gec "pure_numarg" let simple_binding = gec "simple_binding" let simple_binding_list = gec_list "simple_binding_list" let simple_tactic = gec "simple_tactic" let tactic = gec "tactic" - let tactic_com = gec "tactic_com" - let tactic_com_list = gec "tactic_com_list" - let tactic_com_tail = gec "tactic_com_tail" + let tactic_arg = gec "tactic_arg" + let tactic_atom = gec "tactic_atom" + let tactic_expr = gec "tactic_expr" let unfold_occ = gec "unfold_occ" let with_binding_list = gec "with_binding_list" let fixdecl = gec_list "fixdecl" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d7313e296c..a60bfec5e8 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -91,6 +91,7 @@ module Tactic : val autoarg_excluding : Coqast.t Gram.Entry.e val autoarg_usingTDB : Coqast.t Gram.Entry.e val binding_list : Coqast.t Gram.Entry.e + val castedconstrarg : Coqast.t Gram.Entry.e val clausearg : Coqast.t Gram.Entry.e val cofixdecl : Coqast.t list Gram.Entry.e val com_binding_list : Coqast.t list Gram.Entry.e @@ -99,9 +100,14 @@ module Tactic : val constrarg_list : Coqast.t list Gram.Entry.e val fixdecl : Coqast.t list Gram.Entry.e val identarg : Coqast.t Gram.Entry.e + val input_fun : Coqast.t Gram.Entry.e val intropattern : Coqast.t Gram.Entry.e val lconstrarg : Coqast.t Gram.Entry.e val lconstrarg_binding_list : Coqast.t list Gram.Entry.e + val let_clause : Coqast.t Gram.Entry.e + val match_context_rule : Coqast.t Gram.Entry.e + val match_hyps : Coqast.t Gram.Entry.e + val match_rule : Coqast.t Gram.Entry.e val ne_identarg_list : Coqast.t list Gram.Entry.e val ne_intropattern : Coqast.t Gram.Entry.e val ne_num_list : Coqast.t list Gram.Entry.e @@ -113,6 +119,8 @@ module Tactic : val one_intropattern : Coqast.t Gram.Entry.e val pattern_occ : Coqast.t Gram.Entry.e val pattern_occ_hyp : Coqast.t Gram.Entry.e + val pure_numarg : Coqast.t Gram.Entry.e + val rec_clause : Coqast.t Gram.Entry.e val red_flag : Coqast.t Gram.Entry.e val red_tactic : Coqast.t Gram.Entry.e val simple_binding : Coqast.t Gram.Entry.e @@ -120,10 +128,10 @@ module Tactic : val simple_intropattern : Coqast.t Gram.Entry.e val simple_tactic : Coqast.t Gram.Entry.e val tactic : Coqast.t Gram.Entry.e - val tactic_com : Coqast.t Gram.Entry.e - val tactic_com_list : Coqast.t Gram.Entry.e - val tactic_com_tail : Coqast.t Gram.Entry.e + val tactic_arg : Coqast.t Gram.Entry.e + val tactic_atom : Coqast.t Gram.Entry.e val tactic_eoi : Coqast.t Gram.Entry.e + val tactic_expr : Coqast.t Gram.Entry.e val unfold_occ : Coqast.t Gram.Entry.e val with_binding_list : Coqast.t Gram.Entry.e end diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 42d4d91188..8462a72f62 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -213,19 +213,23 @@ let evar_type_case isevars env ct pt lft p c = in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty) *) -let pretype_var loc env id = +let pretype_var loc env lvar id = try - match lookup_id id (context env) with - | RELNAME (n,typ) -> - { uj_val = Rel n; - uj_type = lift n (body_of_type typ); - uj_kind = DOP0 (Sort (level_of_type typ)) } - | GLOBNAME (id,typ) -> - { uj_val = VAR id; - uj_type = body_of_type typ; - uj_kind = DOP0 (Sort (level_of_type typ)) } - with Not_found -> - error_var_not_found_loc loc CCI id + List.assoc id lvar + with + Not_found -> + (try + match lookup_id id (context env) with + | RELNAME (n,typ) -> + { uj_val = Rel n; + uj_type = lift n (body_of_type typ); + uj_kind = DOP0 (Sort (level_of_type typ)) } + | GLOBNAME (id,typ) -> + { uj_val = VAR id; + uj_type = body_of_type typ; + uj_kind = DOP0 (Sort (level_of_type typ)) } + with Not_found -> + error_var_not_found_loc loc CCI id);; (*************************************************************************) (* Main pretyping function *) @@ -233,8 +237,8 @@ let pretype_var loc env id = let trad_metamap = ref [] let trad_nocheck = ref false -let pretype_ref loc isevars env = function -| RVar id -> pretype_var loc env id +let pretype_ref loc isevars env lvar = function +| RVar id -> pretype_var loc env lvar id | RConst (sp,ctxt) -> let cst = (sp,ctxt_of_ids ctxt) in @@ -279,28 +283,32 @@ let pretype_ref loc isevars env = function (* existential variables in constr in environment env with the *) (* constraint vtcon (see Tradevar). *) (* Invariant : Prod and Lambda types are casted !! *) -let rec pretype vtcon env isevars cstr = +let rec pretype vtcon env isevars lvar lmeta cstr = match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) | RRef (loc,ref) -> - pretype_ref loc isevars env ref + pretype_ref loc isevars env lvar ref | RMeta (loc,n) -> - let metaty = - try List.assoc n !trad_metamap - with Not_found -> - (* Tester si la référence est castée *) - user_err_loc - (loc,"pretype", - [< 'sTR "Metavariable "; 'iNT n; 'sTR" is unbound" >]) + (try + List.assoc n lmeta + with + Not_found -> + let metaty = + try List.assoc n !trad_metamap + with Not_found -> + (* Tester si la référence est castée *) + user_err_loc (loc,"pretype", + [< 'sTR "Metavariable "; 'iNT n; 'sTR" is unbound" >]) in - (match kind_of_term metaty with - IsCast (typ,kind) -> {uj_val=DOP0 (Meta n); uj_type=typ; uj_kind=kind} - | _ -> - {uj_val=DOP0 (Meta n); - uj_type=metaty; - uj_kind=failwith "should be casted"}) - (* hnf_constr !isevars (exemeta_hack metaty).uj_type}) *) + (match kind_of_term metaty with + IsCast (typ,kind) -> + {uj_val=DOP0 (Meta n); uj_type=typ; uj_kind=kind} + | _ -> + {uj_val=DOP0 (Meta n); + uj_type=metaty; + uj_kind=failwith "should be casted"})) + (* hnf_constr !isevars (exemeta_hack metaty).uj_type}) *) | RHole loc -> if !compter then nbimpl:=!nbimpl+1; @@ -326,7 +334,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) | RRec (loc,fixkind,lfi,lar,vdef) -> - let larj = Array.map (pretype def_vty_con env isevars) lar in + let larj = Array.map (pretype def_vty_con env isevars lvar lmeta ) lar in let lara = Array.map (assumption_of_judgment env !isevars) larj in let nbfix = Array.length lfi in let lfi = List.map (fun id -> Name id) (Array.to_list lfi) in @@ -337,8 +345,8 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) Array.mapi (fun i def -> (* we lift nbfix times the type in tycon, because of * the nbfix variables pushed to newenv *) - pretype (mk_tycon (lift nbfix (larj.(i).uj_val))) newenv isevars def) - vdef in + pretype (mk_tycon (lift nbfix (larj.(i).uj_val))) newenv isevars lvar + lmeta def) vdef in (evar_type_fixpoint env isevars lfi lara vdefj; match fixkind with | RFix(vn,i) -> @@ -356,10 +364,11 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) { uj_val = dummy_sort; uj_type = dummy_sort; uj_kind = dummy_sort } | RApp (loc,f,args) -> - let j = pretype empty_tycon env isevars f in + let j = pretype empty_tycon env isevars lvar lmeta f in let j = inh_app_fun env isevars j in let apply_one_arg (tycon,jl) c = - let cj = pretype (app_dom_tycon env isevars tycon) env isevars c in + let cj = + pretype (app_dom_tycon env isevars tycon) env isevars lvar lmeta c in let rtc = app_rng_tycon env isevars cj.uj_val tycon in (rtc,cj::jl) in let jl = List.rev (snd (List.fold_left apply_one_arg @@ -367,30 +376,32 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) inh_apply_rel_list !trad_nocheck env isevars jl j vtcon | RBinder(loc,BLambda,name,c1,c2) -> - let j = pretype (abs_dom_valcon env isevars vtcon) env isevars c1 in + let j = + pretype (abs_dom_valcon env isevars vtcon) env isevars lvar lmeta c1 in let assum = inh_ass_of_j env isevars j in let var = (name,assum) in let j' = - pretype (abs_rng_tycon env isevars vtcon) (push_rel var env) isevars c2 + pretype (abs_rng_tycon env isevars vtcon) (push_rel var env) isevars lvar + lmeta c2 in fst (abs_rel env !isevars name assum j') | RBinder(loc,BProd,name,c1,c2) -> - let j = pretype def_vty_con env isevars c1 in + let j = pretype def_vty_con env isevars lvar lmeta c1 in let assum = inh_ass_of_j env isevars j in let var = (name,assum) in - let j' = pretype def_vty_con (push_rel var env) isevars c2 in + let j' = pretype def_vty_con (push_rel var env) isevars lvar lmeta c2 in let j'' = inh_tosort env isevars j' in fst (gen_rel env !isevars name assum j'') | ROldCase (loc,isrec,po,c,lf) -> - let cj = pretype empty_tycon env isevars c in + let cj = pretype empty_tycon env isevars lvar lmeta c in let {mind=mind;params=params;realargs=realargs} = try try_mutind_of env !isevars cj.uj_type with Induc -> error_case_not_inductive CCI env (nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in let pj = match po with - | Some p -> pretype empty_tycon env isevars p + | Some p -> pretype empty_tycon env isevars lvar lmeta p | None -> try match vtcon with (_,(_,Some pred)) -> @@ -406,7 +417,8 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) try let expti = Cases.branch_scheme env isevars isrec i (mind,params) in - let fj = pretype (mk_tycon expti) env isevars lf.(i-1) in + let fj = + pretype (mk_tycon expti) env isevars lvar lmeta lf.(i-1) in let efjt = nf_ise1 !isevars fj.uj_type in let pred = Indrec.pred_case_ml_onebranch env !isevars isrec @@ -430,7 +442,8 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) else let lfj = array_map2 - (fun tyc f -> pretype (mk_tycon tyc) env isevars f) bty lf in + (fun tyc f -> pretype (mk_tycon tyc) env isevars lvar lmeta f) bty + lf in let lfv = (Array.map (fun j -> j.uj_val) lfj) in let lft = (Array.map (fun j -> j.uj_type) lfj) in check_branches_message loc env isevars (cj.uj_val,evalct) (bty,lft); @@ -449,16 +462,15 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) | RCases (loc,prinfo,po,tml,eqns) -> Cases.compile_cases - ((fun vtyc env -> pretype vtyc env isevars),isevars) + ((fun vtyc env -> pretype vtyc env isevars lvar lmeta),isevars) vtcon env (* loc *) (po,tml,eqns) | RCast(loc,c,t) -> - let tj = pretype def_vty_con env isevars t in + let tj = pretype def_vty_con env isevars lvar lmeta t in let tj = inh_tosort_force env isevars tj in let cj = - pretype - (mk_tycon2 vtcon (body_of_type (assumption_of_judgment env !isevars tj))) - env isevars c in + pretype (mk_tycon2 vtcon (body_of_type (assumption_of_judgment env !isevars + tj))) env isevars lvar lmeta c in inh_cast_rel env isevars cj tj (* Maintenant, tout s'exécute... @@ -466,11 +478,11 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) *) -let unsafe_fmachine vtcon nocheck isevars metamap env constr = +let unsafe_fmachine vtcon nocheck isevars metamap env lvar lmeta constr = trad_metamap := metamap; trad_nocheck := nocheck; reset_problems (); - pretype vtcon env isevars constr + pretype vtcon env isevars lvar lmeta constr (* [fail_evar] says how to process unresolved evars: @@ -498,33 +510,42 @@ let j_apply f env sigma j = variables du sigma original. il faudrait que la fonction de typage retourne aussi le nouveau sigma... *) -let ise_resolve_casted sigma env typ c = + +let ise_resolve_casted_gen sigma env lvar lmeta typ c = let isevars = ref sigma in - let j = unsafe_fmachine (mk_tycon typ) false isevars [] env c in + let j = unsafe_fmachine (mk_tycon typ) false isevars [] env lvar lmeta c in (j_apply (fun _ -> process_evars true) env !isevars j).uj_val -let ise_resolve fail_evar sigma metamap env c = +let ise_resolve_casted sigma env typ c = + ise_resolve_casted_gen sigma env [] [] typ c + +(* Raw calls to the inference machine of Trad: boolean says if we must fail + on unresolved evars, or replace them by Metas; the unsafe_judgment list + allows us to extend env with some bindings *) +let ise_resolve fail_evar sigma metamap env lvar lmeta c = let isevars = ref sigma in - let j = unsafe_fmachine empty_tycon false isevars metamap env c in + let j = unsafe_fmachine empty_tycon false isevars metamap env lvar lmeta c in j_apply (fun _ -> process_evars fail_evar) env !isevars j let ise_resolve_type fail_evar sigma metamap env c = let isevars = ref sigma in - let j = unsafe_fmachine def_vty_con false isevars metamap env c in + let j = unsafe_fmachine def_vty_con false isevars metamap env [] [] c in let tj = inh_ass_of_j env isevars j in typed_app (strong (fun _ -> process_evars fail_evar) env !isevars) tj let ise_resolve_nocheck sigma metamap env c = let isevars = ref sigma in - let j = unsafe_fmachine empty_tycon true isevars metamap env c in + let j = unsafe_fmachine empty_tycon true isevars metamap env [] [] c in j_apply (fun _ -> process_evars true) env !isevars j let ise_resolve1 is_ass sigma env c = if is_ass then body_of_type (ise_resolve_type true sigma [] env c) else - (ise_resolve true sigma [] env c).uj_val + (ise_resolve true sigma [] env [] [] c).uj_val +let ise_resolve2 sigma env lmeta lvar c = + (ise_resolve true sigma [] env lmeta lvar c).uj_val;; (* Keeping universe constraints *) (* diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index a20b1eb3f4..9bd4827636 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -12,16 +12,24 @@ open Evarutil (*i*) (* Raw calls to the inference machine of Trad: boolean says if we must fail - * on unresolved evars, or replace them by Metas *) + on unresolved evars, or replace them by Metas ; the unsafe_judgment list + allows us to extend env with some bindings *) val ise_resolve : bool -> 'a evar_map -> (int * constr) list -> - env -> rawconstr -> unsafe_judgment + env -> (identifier * unsafe_judgment) list -> + (int * unsafe_judgment) list -> rawconstr -> unsafe_judgment + val ise_resolve_type : bool -> 'a evar_map -> (int * constr) list -> env -> rawconstr -> typed_type (* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says * if we must coerce to a type *) val ise_resolve1 : bool -> 'a evar_map -> env -> rawconstr -> constr +val ise_resolve2 : 'a evar_map -> env -> (identifier * unsafe_judgment) list -> + (int * unsafe_judgment) list -> rawconstr -> constr +val ise_resolve_casted_gen : + 'a evar_map -> env -> (identifier * unsafe_judgment) list -> + (int * unsafe_judgment) list -> constr -> rawconstr -> constr val ise_resolve_casted : 'a evar_map -> env -> constr -> rawconstr -> constr (* progmach.ml tries to type ill-typed terms: does not perform the conversion @@ -60,6 +68,7 @@ i*) * Unused outside Trad, but useful for debugging *) val pretype : - trad_constraint -> env -> 'a evar_defs -> rawconstr -> unsafe_judgment - + trad_constraint -> env -> 'a evar_defs -> + (identifier * unsafe_judgment) list -> (int * unsafe_judgment) list -> + rawconstr -> unsafe_judgment (*i*) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 51f7e66e30..67c1315246 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -45,7 +45,6 @@ let rec type_of env cstr= with Not_found -> anomaly "type_of: this is not a well-typed term") | IsRel n -> lift n (body_of_type (snd (lookup_rel n env))) | IsVar id -> body_of_type (snd (lookup_var id env)) - | IsAbst _ -> error "No more Abst" (*type_of env (abst_value cstr)*) | IsConst c -> (body_of_type (type_of_constant env sigma c)) | IsEvar _ -> type_of_existential env sigma cstr @@ -67,10 +66,9 @@ let rec type_of env cstr= mkProd name c1 (type_of (push_rel (name,var) env) c2) | IsFix (vn,i,lar,lfi,vdef) -> lar.(i) | IsCoFix (i,lar,lfi,vdef) -> lar.(i) - - | IsAppL(f,args)-> strip_outer_cast (subst_type env sigma (type_of env f) args) + | IsAppL(f,args)-> + strip_outer_cast (subst_type env sigma (type_of env f) args) | IsCast (c,t) -> t - | IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr) | _ -> error "type_of: Unexpected constr" @@ -94,3 +92,9 @@ in type_of, sort_of let get_type_of env sigma = fst (typeur sigma []) env let get_sort_of env sigma = snd (typeur sigma []) env let get_type_of_with_meta env sigma metamap = fst (typeur sigma metamap) env + +(*Makes an unsafe judgment from a constr*) +let mk_unsafe_judgment env evc c= + let typ=get_type_of env evc c + in + {uj_val=c;uj_type=typ;uj_kind=(mkSort (get_sort_of env evc typ))};; diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 3f9ec15552..dd0727b032 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -19,3 +19,6 @@ type metamap = (int * constr) list val get_type_of : env -> 'a evar_map -> constr -> constr val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr val get_sort_of : env -> 'a evar_map -> constr -> sorts + +(*Makes an unsafe judgment from a constr*) +val mk_unsafe_judgment:env->'a evar_map->constr ->unsafe_judgment;; diff --git a/proofs/clenv.ml b/proofs/clenv.ml index e02ffa3b8b..dd5ebb6ef4 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -10,7 +10,7 @@ open Sign open Instantiate open Environ open Evd -open Proof_trees +open Proof_type open Logic open Reduction open Tacmach diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 1f28a73afe..6354a34e37 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -6,7 +6,7 @@ open Util open Names open Term open Tacmach -open Proof_trees +open Proof_type (*i*) (* The Type of Constructions clausale environments. *) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 94f69474b7..91a83ea9d9 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -12,6 +12,7 @@ open Evd open Reduction open Typing open Proof_trees +open Proof_type open Logic open Refiner @@ -58,7 +59,6 @@ let extract_decl sp evc = let restore_decl sp evd evc = let newctxt = { lc = (ts_it evc).focus; - mimick = (get_mimick evd); pgm = (get_pgm evd) } in let newgoal = { evar_env = evd.evar_env; evar_concl = evd.evar_concl; diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 620c9c4b8c..1674f2f3ac 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -8,6 +8,7 @@ open Sign open Environ open Evd open Proof_trees +open Proof_type open Refiner (*i*) diff --git a/proofs/logic.ml b/proofs/logic.ml index 71e79a7913..3270177ee1 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -12,6 +12,7 @@ open Environ open Reduction open Typing open Proof_trees +open Proof_type open Typeops open Type_errors open Coqast diff --git a/proofs/logic.mli b/proofs/logic.mli index 7df383a738..31f0b51999 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -7,7 +7,7 @@ open Term open Sign open Evd open Environ -open Proof_trees +open Proof_type (*i*) (* The primitive refiner. *) diff --git a/proofs/macros.ml b/proofs/macros.ml index de6132f36f..95da5702d5 100644 --- a/proofs/macros.ml +++ b/proofs/macros.ml @@ -5,7 +5,7 @@ open Pp open Util open Names open Term -open Proof_trees +open Proof_type open Libobject open Library open Coqast diff --git a/proofs/macros.mli b/proofs/macros.mli index c62f13c76c..a237d3fd73 100644 --- a/proofs/macros.mli +++ b/proofs/macros.mli @@ -4,7 +4,7 @@ (*i*) open Names open Tacmach -open Proof_trees +open Proof_type (*i*) (* This file contains the table of macro tactics. The body of the diff --git a/proofs/pattern.ml b/proofs/pattern.ml index a30a829927..983154c80f 100644 --- a/proofs/pattern.ml +++ b/proofs/pattern.ml @@ -100,9 +100,12 @@ let head_of_constr_reference = function *) +exception PatternMatchingFailure + let constrain ((n : int),(m : constr)) sigma = if List.mem_assoc n sigma then - if eq_constr m (List.assoc n sigma) then sigma else error "somatch" + if eq_constr m (List.assoc n sigma) then sigma + else raise PatternMatchingFailure else (n,m)::sigma @@ -124,8 +127,6 @@ let memb_metavars m n = let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2 -exception PatternMatchingFailure - let matches_core convert pat c = let rec sorec stk sigma p t = let cT = whd_castapp t in @@ -180,6 +181,9 @@ let matches_core convert pat c = | PBinder(BLambda,na1,c1,d1), IsLambda(na2,c2,d2) -> sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2 + | PRef (RConst (sp1,ctxt1)), IsConst (sp2,ctxt2) + when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma + | PRef (RConst (sp1,ctxt1)), _ when convert <> None -> let (env,evars) = out_some convert in if is_conv env evars (mkConst (sp1,ctxt1)) cT then sigma diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index a8b8ba97ec..7ffb408786 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -14,6 +14,7 @@ open Declare open Typing open Tacmach open Proof_trees +open Proof_type open Lib open Astterm diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 13f7b6c1c1..3499f9227b 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -8,7 +8,7 @@ open Term open Sign open Environ open Declare -open Proof_trees +open Proof_type open Tacmach (*i*) diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index f4990659c6..446d4b2a29 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -8,85 +8,9 @@ open Sign open Evd open Stamps open Environ +open Proof_type open Typing -type bindOcc = - | Dep of identifier - | NoDep of int - | Com - -type 'a substitution = (bindOcc * 'a) list - -type tactic_arg = - | Command of Coqast.t - | Constr of constr - | Identifier of identifier - | Integer of int - | Clause of identifier list - | Bindings of Coqast.t substitution - | Cbindings of constr substitution - | Quoted_string of string - | Tacexp of Coqast.t - | Redexp of string * Coqast.t list - | Fixexp of identifier * int * Coqast.t - | Cofixexp of identifier * Coqast.t - | Letpatterns of int list option * (identifier * int list) list - | Intropattern of intro_pattern - -and intro_pattern = - | IdPat of identifier - | DisjPat of intro_pattern list - | ConjPat of intro_pattern list - | ListPat of intro_pattern list - -and tactic_expression = string * tactic_arg list - - -type pf_status = Complete_proof | Incomplete_proof - -type prim_rule_name = - | Intro - | Intro_after - | Intro_replacing - | Fix - | Cofix - | Refine - | Convert_concl - | Convert_hyp - | Thin - | Move of bool - -type prim_rule = { - name : prim_rule_name; - hypspecs : identifier list; - newids : identifier list; - params : Coqast.t list; - terms : constr list } - -type local_constraints = Intset.t - -type proof_tree = { - status : pf_status; - goal : goal; - ref : (rule * proof_tree list) option; - subproof : proof_tree option } - -and goal = ctxtty evar_info - -and rule = - | Prim of prim_rule - | Tactic of tactic_expression - | Context of ctxtty - | Local_constraints of local_constraints - -and ctxtty = { - pgm : constr option; - mimick : proof_tree option; - lc : local_constraints } - -type evar_declarations = ctxtty evar_map - - let is_bind = function | Bindings _ -> true | _ -> false @@ -101,7 +25,7 @@ let mk_goal ctxt env cl = (* Functions on the information associated with existential variables *) -let mt_ctxt lc = { pgm = None; mimick = None; lc = lc } +let mt_ctxt lc = { pgm = None; lc = lc } let get_ctxt gl = out_some gl.evar_info @@ -109,10 +33,6 @@ let get_pgm gl = (out_some gl.evar_info).pgm let set_pgm pgm ctxt = { ctxt with pgm = pgm } -let get_mimick gl = (out_some gl.evar_info).mimick - -let set_mimick mimick ctxt = { mimick = mimick; pgm = ctxt.pgm; lc = ctxt.lc } - let get_lc gl = (out_some gl.evar_info).lc (* Functions on proof trees *) @@ -442,7 +362,7 @@ let ast_of_cvt_arg = function (ast_of_cvt_bind (ast_of_constr false (assumptions_for_print []))) bl) | Tacexp ast -> ope ("TACTIC",[ast]) - | Redexp (s,args) -> ope ("REDEXP", [ope(s,args)]) + | Redexp red -> failwith "TODO: ast_of_cvt_arg: Redexp" | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id)); (num n); ope ("COMMAND",[c])]) diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 6aa76f617f..60ae9b4f4c 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -9,95 +9,11 @@ open Term open Sign open Evd open Environ +open Proof_type (*i*) -(* This module declares the structures of proof trees, global and - readable constraints, and a few utilities on these types *) - -type bindOcc = - | Dep of identifier - | NoDep of int - | Com - -type 'a substitution = (bindOcc * 'a) list - -type tactic_arg = - | Command of Coqast.t - | Constr of constr - | Identifier of identifier - | Integer of int - | Clause of identifier list - | Bindings of Coqast.t substitution - | Cbindings of constr substitution - | Quoted_string of string - | Tacexp of Coqast.t - | Redexp of string * Coqast.t list - | Fixexp of identifier * int * Coqast.t - | Cofixexp of identifier * Coqast.t - | Letpatterns of int list option * (identifier * int list) list - | Intropattern of intro_pattern - -and intro_pattern = - | IdPat of identifier - | DisjPat of intro_pattern list - | ConjPat of intro_pattern list - | ListPat of intro_pattern list - -and tactic_expression = string * tactic_arg list - - -type pf_status = Complete_proof | Incomplete_proof - -type prim_rule_name = - | Intro - | Intro_after - | Intro_replacing - | Fix - | Cofix - | Refine - | Convert_concl - | Convert_hyp - | Thin - | Move of bool - -type prim_rule = { - name : prim_rule_name; - hypspecs : identifier list; - newids : identifier list; - params : Coqast.t list; - terms : constr list } - -type local_constraints = Intset.t - -(*s Proof trees. - [ref] = [None] if the goal has still to be proved, - and [Some (r,l)] if the rule [r] was applied to the goal - and gave [l] as subproofs to be completed. - [subproof] = [(Some p)] if [ref = (Some(Tactic t,l))]; - [p] is then the proof that the goal can be proven if the goals - in [l] are solved. *) - -type proof_tree = { - status : pf_status; - goal : goal; - ref : (rule * proof_tree list) option; - subproof : proof_tree option } - -and goal = ctxtty evar_info - -and rule = - | Prim of prim_rule - | Tactic of tactic_expression - | Context of ctxtty - | Local_constraints of local_constraints - -and ctxtty = { - pgm : constr option; - mimick : proof_tree option; - lc : local_constraints } - -type evar_declarations = ctxtty evar_map - +(* This module declares readable constraints, and a few utilities on + constraints and proof trees *) val mk_goal : ctxtty -> env -> constr -> goal @@ -105,8 +21,6 @@ val mt_ctxt : local_constraints -> ctxtty val get_ctxt : goal -> ctxtty val get_pgm : goal -> constr option val set_pgm : constr option -> ctxtty -> ctxtty -val get_mimick : goal -> proof_tree option -val set_mimick : proof_tree option -> ctxtty -> ctxtty val get_lc : goal -> local_constraints val rule_of_proof : proof_tree -> rule diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml new file mode 100644 index 0000000000..eaebd6b992 --- /dev/null +++ b/proofs/proof_type.ml @@ -0,0 +1,106 @@ +(*i*) +open Environ +open Evd +open Names +open Stamps +open Term +open Util +(*i*) + +(*This module defines the structure of proof tree and the tactic type. So, it + is used by Proof_tree and Refiner*) + +type bindOcc = + | Dep of identifier + | NoDep of int + | Com + +type 'a substitution = (bindOcc * 'a) list + +type pf_status = Complete_proof | Incomplete_proof + +type prim_rule_name = + | Intro + | Intro_after + | Intro_replacing + | Fix + | Cofix + | Refine + | Convert_concl + | Convert_hyp + | Thin + | Move of bool + +type prim_rule = { + name : prim_rule_name; + hypspecs : identifier list; + newids : identifier list; + params : Coqast.t list; + terms : constr list } + +type local_constraints = Intset.t + +type ctxtty = { + pgm : constr option; + lc : local_constraints } + +type evar_declarations = ctxtty evar_map + +(* A global constraint is a mappings of existential variables + with some extra information for the program tactic *) +type global_constraints = evar_declarations timestamped + +(*Signature useful to define the tactic type*) +type 'a sigma = { + it : 'a ; + sigma : global_constraints } + +(*s Proof trees. + [ref] = [None] if the goal has still to be proved, + and [Some (r,l)] if the rule [r] was applied to the goal + and gave [l] as subproofs to be completed. + [subproof] = [(Some p)] if [ref = (Some(Tactic t,l))]; + [p] is then the proof that the goal can be proven if the goals + in [l] are solved. *) +type proof_tree = { + status : pf_status; + goal : goal; + ref : (rule * proof_tree list) option; + subproof : proof_tree option } + +and rule = + | Prim of prim_rule + | Tactic of tactic_expression + | Context of ctxtty + | Local_constraints of local_constraints + +and goal = ctxtty evar_info + +and tactic = goal sigma -> (goal list sigma * validation) + +and validation = (proof_tree list -> proof_tree) + +and tactic_arg = + Command of Coqast.t + | Constr of constr + | Identifier of identifier + | Integer of int + | Clause of identifier list + | Bindings of Coqast.t substitution + | Cbindings of constr substitution + | Quoted_string of string + | Tacexp of Coqast.t + | Tac of tactic + | Redexp of Tacred.red_expr + | Fixexp of identifier * int * Coqast.t + | Cofixexp of identifier * Coqast.t + | Letpatterns of (int list option * (identifier * int list) list) + | Intropattern of intro_pattern + +and intro_pattern = + | IdPat of identifier + | DisjPat of intro_pattern list + | ConjPat of intro_pattern list + | ListPat of intro_pattern list + +and tactic_expression = string * tactic_arg list diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli new file mode 100644 index 0000000000..eaebd6b992 --- /dev/null +++ b/proofs/proof_type.mli @@ -0,0 +1,106 @@ +(*i*) +open Environ +open Evd +open Names +open Stamps +open Term +open Util +(*i*) + +(*This module defines the structure of proof tree and the tactic type. So, it + is used by Proof_tree and Refiner*) + +type bindOcc = + | Dep of identifier + | NoDep of int + | Com + +type 'a substitution = (bindOcc * 'a) list + +type pf_status = Complete_proof | Incomplete_proof + +type prim_rule_name = + | Intro + | Intro_after + | Intro_replacing + | Fix + | Cofix + | Refine + | Convert_concl + | Convert_hyp + | Thin + | Move of bool + +type prim_rule = { + name : prim_rule_name; + hypspecs : identifier list; + newids : identifier list; + params : Coqast.t list; + terms : constr list } + +type local_constraints = Intset.t + +type ctxtty = { + pgm : constr option; + lc : local_constraints } + +type evar_declarations = ctxtty evar_map + +(* A global constraint is a mappings of existential variables + with some extra information for the program tactic *) +type global_constraints = evar_declarations timestamped + +(*Signature useful to define the tactic type*) +type 'a sigma = { + it : 'a ; + sigma : global_constraints } + +(*s Proof trees. + [ref] = [None] if the goal has still to be proved, + and [Some (r,l)] if the rule [r] was applied to the goal + and gave [l] as subproofs to be completed. + [subproof] = [(Some p)] if [ref = (Some(Tactic t,l))]; + [p] is then the proof that the goal can be proven if the goals + in [l] are solved. *) +type proof_tree = { + status : pf_status; + goal : goal; + ref : (rule * proof_tree list) option; + subproof : proof_tree option } + +and rule = + | Prim of prim_rule + | Tactic of tactic_expression + | Context of ctxtty + | Local_constraints of local_constraints + +and goal = ctxtty evar_info + +and tactic = goal sigma -> (goal list sigma * validation) + +and validation = (proof_tree list -> proof_tree) + +and tactic_arg = + Command of Coqast.t + | Constr of constr + | Identifier of identifier + | Integer of int + | Clause of identifier list + | Bindings of Coqast.t substitution + | Cbindings of constr substitution + | Quoted_string of string + | Tacexp of Coqast.t + | Tac of tactic + | Redexp of Tacred.red_expr + | Fixexp of identifier * int * Coqast.t + | Cofixexp of identifier * Coqast.t + | Letpatterns of (int list option * (identifier * int list) list) + | Intropattern of intro_pattern + +and intro_pattern = + | IdPat of identifier + | DisjPat of intro_pattern list + | ConjPat of intro_pattern list + | ListPat of intro_pattern list + +and tactic_expression = string * tactic_arg list diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 3af8748035..9e1698c25c 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -13,14 +13,9 @@ open Reduction open Instantiate open Type_errors open Proof_trees +open Proof_type open Logic -type 'a sigma = { - it : 'a ; - sigma : global_constraints } - -type validation = (proof_tree list -> proof_tree) -type tactic = goal sigma -> (goal list sigma * validation) type transformation_tactic = proof_tree -> (goal list * validation) let hypotheses gl = gl.evar_env diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 4d1edc7e5b..d0b3ca33ab 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -5,14 +5,11 @@ open Term open Sign open Proof_trees +open Proof_type (*i*) (* The refiner (handles primitive rules and high-level tactics). *) -type 'a sigma = { - it : 'a ; - sigma : global_constraints } - val sig_it : 'a sigma -> 'a val sig_sig : 'a sigma -> global_constraints @@ -23,10 +20,6 @@ val repackage : global_constraints ref -> 'a -> 'a sigma val apply_sig_tac : global_constraints ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c -type validation = (proof_tree list -> proof_tree) - -type tactic = goal sigma -> (goal list sigma * validation) - type transformation_tactic = proof_tree -> (goal list * validation) val add_tactic : string -> (tactic_arg list -> tactic) -> unit diff --git a/tactics/stock.ml b/proofs/stock.ml index ef0feec952..ef0feec952 100644 --- a/tactics/stock.ml +++ b/proofs/stock.ml diff --git a/tactics/stock.mli b/proofs/stock.mli index c0cd43c7d5..c0cd43c7d5 100644 --- a/tactics/stock.mli +++ b/proofs/stock.mli diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 9e6f3006ea..0343895491 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -1,134 +1,703 @@ (* $Id$ *) +open Astterm +open Closure +open Generic +open Libobject +open Pattern open Pp +open Rawterm +open Sign +open Tacred open Util open Names -open Term -open Proof_trees +open Proof_type open Tacmach open Macros open Coqast open Ast +open Term +let err_msg_tactic_not_found macro_loc macro = + user_err_loc + (macro_loc,"macro_expand", + [< 'sTR"Tactic macro ";'sTR macro; 'sPC; 'sTR"not found" >]) -let tactic_tab = - (Hashtbl.create 17 : (string, tactic_arg list -> tactic) Hashtbl.t) +(*Values for interpretation*) +type value= + VTactic of tactic + |VFTactic of tactic_arg list*(tactic_arg list->tactic) + |VRTactic of (goal list sigma * validation) + |VArg of tactic_arg + |VFun of (string*value) list*string option list*Coqast.t + |VVoid + |VRec of value ref;; -let tacinterp_add (s,f) = - try - Hashtbl.add tactic_tab s f - with Failure _ -> - errorlabstrm "tacinterp_add" - [< 'sTR"Cannot add the tactic " ; 'sTR s ; 'sTR" twice" >] - -let overwriting_tacinterp_add (s,f) = - if Hashtbl.mem tactic_tab s then begin - Hashtbl.remove tactic_tab s; - warning ("Overwriting definition of tactic interpreter command "^s) - end; - Hashtbl.add tactic_tab s f +(*Gives the identifier corresponding to an Identifier tactic_arg*) +let id_of_Identifier=function + Identifier id -> id + |_ -> + anomalylabstrm "id_of_IDENTIFIER" [<'sTR "Not an IDENTIFIER tactic_arg">];; -let tacinterp_init () = Hashtbl.clear tactic_tab +(*Gives the constr corresponding to a Constr tactic_arg*) +let constr_of_Constr=function + Constr c -> c + |_ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a CONSTR tactic_arg">];; -let tacinterp_map s = Hashtbl.find tactic_tab s +(*Signature for interpretation: val_interp and interpretation functions*) +type interp_sign= + evar_declarations*Environ.env*(string*value) list*(int*constr) list* + goal sigma option;; -let err_msg_tactic_not_found macro_loc macro = - user_err_loc - (macro_loc,"macro_expand", - [< 'sTR"Tactic macro ";'sTR macro; 'sPC; 'sTR"not found" >]) +(*Table of interpretation functions*) +let interp_tab= + (Hashtbl.create 17:(string,interp_sign->Coqast.t->value) Hashtbl.t);; + +(*Adds an interpretation function*) +let interp_add (ast_typ,interp_fun)= + try + Hashtbl.add interp_tab ast_typ interp_fun + with + Failure _ -> + errorlabstrm "interp_add" [<'sTR + "Cannot add the interpretation function for "; 'sTR ast_typ; 'sTR + " twice">];; + +(*Adds a possible existing interpretation function*) +let overwriting_interp_add (ast_typ,interp_fun)= + if Hashtbl.mem interp_tab ast_typ then + (Hashtbl.remove interp_tab ast_typ; + warning ("Overwriting definition of tactic interpreter command "^ast_typ)); + Hashtbl.add interp_tab ast_typ interp_fun;; + +(*Finds the interpretation function corresponding to a given ast type*) +let look_for_interp=Hashtbl.find interp_tab;; + +(*Globalizes the identifier*) +let glob_nvar id= + try + Nametab.sp_of_id CCI id + with + Not_found -> error ("unbound variable "^(string_of_id id));; + +(*Summary and Object declaration*) +let mactab=ref Gmap.empty;; + +let lookup id=Gmap.find id !mactab;; + +let init ()=mactab:=Gmap.empty in +let freeze ()= !mactab in +let unfreeze fs=mactab:=fs in + Summary.declare_summary "tactic-definition" + {Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init};; + +let (inMD,outMD)= + let add (na,td)=mactab:=Gmap.add na td !mactab in + let cache_md (_,(na,td))=add (na,td) in + declare_object ("TACTIC-DEFINITION", + {cache_function=cache_md; + load_function=(fun _ -> ()); + open_function=(fun _ -> ()); + specification_function=(fun x -> x)});; + +(*Adds a Tactic Definition in the table*) +let add_tacdef na vbody= + if Gmap.mem na !mactab then + errorlabstrm "Tacdef.add_tacdef" [<'sTR + "There is already a Tactic Definition named "; 'sTR na>] + else + let _=Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) + in + mSGNL [<'sTR (na^" is defined")>];; + +(*Unboxes the tactic_arg*) +let unvarg=function + VArg a -> a + |_ -> errorlabstrm "unvarg" [<'sTR "Not a tactic argument">];; + +(*Unboxes VRec*) +let unrec=function + VRec v -> !v + |a -> a;; + +(*Unboxes REDEXP*) +let unredexp=function + Redexp c -> c + |_ -> errorlabstrm "unredexp" [<'sTR "Not a REDEXP tactic_arg">];; + +(*Reads the head of Fun*) +let read_fun ast= + let rec read_fun_rec=function + Node(_,"VOID",[])::tl -> None::(read_fun_rec tl) + |Nvar(_,s)::tl -> (Some s)::(read_fun_rec tl) + |[] -> [] + |_ -> + anomalylabstrm "Tacinterp.read_fun_rec" [<'sTR "Fun not well formed">] + in + match ast with + Node(_,"FUNVAR",l) -> read_fun_rec l + |_ -> + anomalylabstrm "Tacinterp.read_fun" [<'sTR "Fun not well formed">];; + +(*Reads the clauses of a Rec*) +let rec read_rec_clauses=function + [] -> [] + |Node(_,"RECCLAUSE",[Nvar(_,name);it;body])::tl -> + (name,it,body)::(read_rec_clauses tl) + |_ -> + anomalylabstrm "Tacinterp.read_rec_clauses" [<'sTR + "Rec not well formed">];; + +(*Associates variables with values and gives the remaining variables and + values*) +let head_with_value (lvar,lval)= + let rec head_with_value_rec lacc=function + ([],[]) -> (lacc,[],[]) + |(vr::tvr,ve::tve) -> + (match vr with + None -> head_with_value_rec lacc (tvr,tve) + |Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve)) + |(vr,[]) -> (lacc,vr,[]) + |([],ve) -> (lacc,[],ve) + in + head_with_value_rec [] (lvar,lval);; + +(*Type of hypotheses for a Match Context rule*) +type match_context_hyps= + NoHypId of constr_pattern + |Hyp of string*constr_pattern;; + +(*Type of a Match rule for Match Context and Match*) +type match_rule= + Pat of match_context_hyps list*constr_pattern*Coqast.t + |All of Coqast.t;; + +(*Gives the ast of a COMMAND ast node*) +let ast_of_command=function + Node(_,"COMMAND",[c]) -> c + |ast -> + anomaly_loc (Ast.loc ast, "Tacinterp.ast_of_command",[<'sTR + "Not a COMMAND ast node: ";print_ast ast>]);; + +(*Reads the hypotheses of a Match Context rule*) +let rec read_match_context_hyps evc env=function + Node(_,"MATCHCONTEXTHYPS",[pc])::tl -> + (NoHypId (snd (interp_constrpattern evc env (ast_of_command + pc))))::(read_match_context_hyps evc env tl) + |Node(_,"MATCHCONTEXTHYPS",[Nvar(_,s);pc])::tl -> + (Hyp (s,snd (interp_constrpattern evc env (ast_of_command + pc))))::(read_match_context_hyps evc env tl) + |ast::tl -> + anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_hyp",[<'sTR + "Not a MATCHCONTEXTHYP ast node: ";print_ast ast>]) + |[] -> [];; + +(*Reads the rules of a Match Context*) +let rec read_match_context_rule evc env=function + Node(_,"MATCHCONTEXTRULE",[tc])::tl -> + (All tc)::(read_match_context_rule evc env tl) + |Node(_,"MATCHCONTEXTRULE",l)::tl -> + let rl=List.rev l + in + (Pat (read_match_context_hyps evc env (List.tl (List.tl rl)),snd + (interp_constrpattern evc env (ast_of_command (List.nth rl + 1))),List.hd rl))::(read_match_context_rule evc env tl) + |ast::tl -> + anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR + "Not a MATCHCONTEXTRULE ast node: ";print_ast ast>]) + |[] -> [];; + +(*Reads the rules of a Match*) +let rec read_match_rule evc env=function + Node(_,"MATCHRULE",[te])::tl -> + (All te)::(read_match_rule evc env tl) + |Node(_,"MATCHRULE",[com;te])::tl -> + (Pat ([],snd (interp_constrpattern evc env (ast_of_command + com)),te))::(read_match_rule evc env tl) + |ast::tl -> + anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR + "Not a MATCHRULE ast node: ";print_ast ast>]) + |[] -> [];; + +(*Transforms a type_judgment signature into a (string*constr) list*) +let make_hyps hyps= + let lid=List.map string_of_id (ids_of_sign hyps) + and lhyp=List.map body_of_type (vals_of_sign hyps) + in + List.combine lid lhyp;; + +(*For Match Context and Match*) +exception No_match;; +exception Not_coherent_metas;; + +(*Verifies if the matched list is coherent with respect to lcm*) +let rec verify_metas_coherence lcm=function + (num,csr)::tl -> + if (List.for_all + (fun (a,b) -> + if a=num then + eq_constr b csr + else + true) lcm) then + (num,csr)::(verify_metas_coherence lcm tl) + else + raise Not_coherent_metas + |[] -> [];; + +(*Tries to match a pattern and a constr*) +let apply_matching pat csr= + try + (Pattern.matches pat csr) + with + PatternMatchingFailure -> raise No_match;; + +(*Tries to match one hypothesis with a list of hypothesis patterns*) +let apply_one_hyp_context lmatch mhyps (idhyp,hyp)= + let rec apply_one_hyp_context_rec (idhyp,hyp) mhyps_acc=function + (Hyp (idpat,pat))::tl -> + (try + ([idpat,VArg (Identifier + (id_of_string idhyp))],verify_metas_coherence lmatch + (Pattern.matches pat hyp),mhyps_acc@tl) + with + PatternMatchingFailure|Not_coherent_metas -> + apply_one_hyp_context_rec (idhyp,hyp) (mhyps_acc@[Hyp + (idpat,pat)]) tl) + |(NoHypId pat)::tl -> + (try + ([],verify_metas_coherence lmatch (Pattern.matches pat + hyp),mhyps_acc@tl) + with + PatternMatchingFailure|Not_coherent_metas -> + apply_one_hyp_context_rec (idhyp,hyp) (mhyps_acc@[NoHypId pat]) + tl) + |[] -> raise No_match + in + apply_one_hyp_context_rec (idhyp,hyp) [] mhyps;; + +(*Prepares the lfun list for constr substitutions*) +let rec make_subs_list=function + (id,VArg (Identifier i))::tl -> + (id_of_string id,VAR i)::(make_subs_list tl) + |(id,VArg (Constr c))::tl -> + (id_of_string id,c)::(make_subs_list tl) + |e::tl -> make_subs_list tl + |[] -> [];; + +(*Interprets any expression*) +let rec val_interp (evc,env,lfun,lmatch,goalopt) ast= +(* mSGNL [<print_ast ast>];*) + +(*mSGNL [<print_ast (Termast.bdize false (Pretty.assumptions_for_print []) ((reduction_of_redexp redexp) env evc c))>];*) + + match ast with + Node(_,"APP",l) -> + let fv=val_interp (evc,env,lfun,lmatch,goalopt) (List.hd l) + and largs= + List.map (val_interp (evc,env,lfun,lmatch,goalopt)) (List.tl l) + in + app_interp evc env lfun lmatch goalopt fv largs ast + |Node(_,"FUN",l) -> VFun (lfun,read_fun (List.hd l),List.nth l 1) + |Node(_,"REC",l) -> rec_interp evc env lfun lmatch goalopt ast l + |Node(_,"LET",[Node(_,"LETDECL",l);u]) -> + let addlfun=let_interp evc env lfun lmatch goalopt ast l + in + val_interp (evc,env,(lfun@addlfun),lmatch,goalopt) u + |Node(_,"MATCHCONTEXT",lmr) -> + match_context_interp evc env lfun lmatch goalopt ast lmr + |Node(_,"MATCH",lmr) -> + match_interp evc env lfun lmatch goalopt ast lmr + |Node(_,"IDTAC",[]) -> VTactic tclIDTAC + |Node(_,"FAIL",[]) -> VTactic tclFAIL + |Node(_,"TACTICLIST",l) -> + VTactic (interp_semi_list tclIDTAC lfun lmatch l) + |Node(_,"DO",[n;tac]) -> + VTactic (tclDO (num_of_ast n) (tac_interp lfun lmatch tac)) + |Node(_,"TRY",[tac]) -> + VTactic (tclTRY (tac_interp lfun lmatch tac)) + |Node(_,"INFO",[tac]) -> + VTactic (tclINFO (tac_interp lfun lmatch tac)) + |Node(_,"REPEAT",[tac]) -> + VTactic (tclREPEAT (tac_interp lfun lmatch tac)) + |Node(_,"ORELSE",[tac1;tac2]) -> + VTactic (tclORELSE (tac_interp lfun lmatch tac1) (tac_interp lfun lmatch + tac2)) + |Node(_,"FIRST",l) -> + VTactic (tclFIRST (List.map (tac_interp lfun lmatch) l)) + |Node(_,"TCLSOLVE",l) -> + VTactic (tclSOLVE (List.map (tac_interp lfun lmatch) l)) + |Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) -> + val_interp (evc,env,lfun,lmatch,goalopt) (Node(loc0,"APP",[Node(loc1, + "PRIM-TACTIC",[Node(loc1,s,[])])]@l)) + |Node(_,"PRIM-TACTIC",[Node(loc,opn,[])]) -> + VFTactic ([],(interp_atomic loc opn)) + |Node(_,"VOID",[]) -> VVoid + |Nvar(_,s) -> + (try + (unrec (List.assoc s (List.rev lfun))) + with + Not_found -> + (try + (lookup s) + with + Not_found -> VArg (Identifier (id_of_string s)))) + |Str(_,s) -> VArg (Quoted_string s) + |Num(_,n) -> VArg (Integer n) + |Node(_,"COMMAND",[c]) -> com_interp (evc,env,lfun,lmatch,goalopt) c + |Node(_,"CASTEDCOMMAND",[c]) -> + cast_com_interp (evc,env,lfun,lmatch,goalopt) c + |Node(_,"BINDINGS",astl) -> + VArg (Cbindings (List.map (bind_interp evc env lfun lmatch goalopt) + astl)) + |Node(_,"REDEXP",[Node(_,redname,args)]) -> + VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt) + (redname,args))) + |Node(_,"CLAUSE",cl) -> + VArg (Clause (List.map (fun ast -> id_of_Identifier (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt) ast))) cl)) + |Node(_,"TACTIC",[ast]) -> VArg (Tac (tac_interp lfun lmatch ast)) +(*Remains to treat*) + |Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) -> + VArg ((Fixexp (id_of_string s,n,c))) + |Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) -> + VArg ((Cofixexp (id_of_string s,c))) +(*End of Remains to treat*) + |Node(_,"INTROPATTERN", [ast]) -> + VArg ((Intropattern (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt) + ast))) + |Node(_,"LETPATTERNS",astl) -> + VArg (Letpatterns (List.fold_left (cvt_letpattern + (evc,env,lfun,lmatch,goalopt)) (None,[]) astl)) + |Node(loc,s,l) -> + (try + ((look_for_interp s) (evc,env,lfun,lmatch,goalopt) ast) + with + Not_found -> + val_interp (evc,env,lfun,lmatch,goalopt) + (Node(dummy_loc,"APPTACTIC",[ast]))) + |_ -> + anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",[<'sTR + "Unrecognizable ast: ";print_ast ast>]) +(*Interprets an application node*) +and app_interp evc env lfun lmatch goalopt fv largs ast= + match fv with + VFTactic(l,f) -> VFTactic(l@(List.map unvarg largs),f) + |VFun(olfun,var,body) -> + let (newlfun,lvar,lval)=head_with_value (var,largs) + in + if lvar=[] then + if lval=[] then + val_interp (evc,env,(olfun@newlfun),lmatch,goalopt) body + else + app_interp evc env lfun lmatch goalopt (val_interp (evc,env, + (olfun@newlfun),lmatch,goalopt) body) lval ast + else + VFun(olfun@newlfun,lvar,body) + |_ -> + anomaly_loc (Ast.loc ast, "Tacinterp.app_interp",[<'sTR + "Illegal application: "; print_ast ast>]) +(*Interprets recursive expressions*) +and rec_interp evc env lfun lmatch goalopt ast=function + [Node(_,"RECCLAUSE",_)] as l -> + let (name,var,body)=List.hd (read_rec_clauses l) + and ve=ref VVoid + in + let newve= + VFun(lfun@[(name,VRec ve)],read_fun var,body) + in + ve:=newve; + !ve + |[Node(_,"RECDECL",l);u] -> + let lrc=read_rec_clauses l + in + let lref=Array.to_list (Array.make (List.length lrc) (ref VVoid)) + in + let lenv= + List.fold_right2 (fun (name,_,_) vref l -> (name,VRec vref)::l) lrc + lref [] + in + let lve= + List.map (fun (name,var,body) -> (name,VFun(lfun@lenv,read_fun + var,body))) lrc + in + List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve; + val_interp (evc,env,(lfun@lve),lmatch,goalopt) u + |_ -> + anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",[<'sTR + "Rec not well formed: "; print_ast ast>]) +(*Interprets the clauses of a let*) +and let_interp evc env lfun lmatch goalopt ast=function + [] -> [] + |Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl -> + (id,val_interp (evc,env,lfun,lmatch,goalopt) t)::(let_interp evc env lfun + lmatch goalopt ast tl) + |_ -> + anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",[<'sTR + "Let not well formed: "; print_ast ast>]) +(*Interprets the Match Context expressions*) +and match_context_interp evc env lfun lmatch goalopt ast lmr= + let rec apply_match_context evc env lfun lmatch goalopt=function + (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t + |(Pat (mhyps,mgoal,mt))::tl -> + (match goalopt with + None -> + errorlabstrm "Tacinterp.apply_match_context" [<'sTR + "No goal available">] + |Some g -> + let hyps=make_hyps (pf_hyps g) + and concl=pf_concl g + in + try + (let lgoal=apply_matching mgoal concl + in + if mhyps=[] then + val_interp (evc,env,lfun,lgoal@lmatch,goalopt) mt + else + apply_hyps_context evc env lfun lmatch g mt lgoal mhyps + hyps) + with + No_match -> + apply_match_context evc env lfun lmatch goalopt tl) + |_ -> + errorlabstrm "Tacinterp.apply_match_context" [<'sTR + "No matching clauses for Match Context">] + in + apply_match_context evc env lfun lmatch goalopt (read_match_context_rule + evc env lmr) +(*Tries to match the hypotheses in a Match Context*) +and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps + hyps= + let rec apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun + lmatch mhyps hyps hyps_acc= + match hyps with + hd::tl -> + (try + (let (lid,lm,newmhyps)=apply_one_hyp_context lmatch mhyps hd + in + if newmhyps=[] then + match + (val_interp (evc,env,(lfun@lid@lfun_glob), + (lmatch@lm@lmatch_glob),Some goal) mt) with + VTactic tac -> VRTactic (tac goal) + |VFTactic (largs,f) -> VRTactic (f largs goal) + |a -> a + else + apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt + (lfun@lid) (lmatch@lm) newmhyps (hyps_acc@tl) []) + with + No_match | _ -> + apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt + lfun lmatch mhyps tl (hyps_acc@[hd])) + |[] -> raise No_match + in + apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt [] lgmatch + mhyps hyps [] +(*Interprets the Match expressions*) +and match_interp evc env lfun lmatch goalopt ast lmr= + let rec apply_match evc env lfun lmatch goalopt csr=function + (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t + |(Pat ([],mc,mt))::tl -> + (try + (let lcsr=apply_matching mc csr + in + val_interp (evc,env,lfun,(apply_matching mc csr)@lmatch,goalopt) + mt) + with + No_match -> apply_match evc env lfun lmatch goalopt csr tl) + |_ -> + errorlabstrm "Tacinterp.apply_match" [<'sTR + "No matching clauses for Match">] + in + let csr= + constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) + (List.hd lmr))) + and ilr=read_match_rule evc env (List.tl lmr) + in + apply_match evc env lfun lmatch goalopt csr ilr +(*Interprets tactic expressions*) +and tac_interp lfun lmatch ast g= + let evc=project g + and env=pf_env g + in + match (val_interp (evc,env,lfun,lmatch,(Some g)) ast) with + VTactic tac -> (tac g) + |VFTactic (largs,f) -> (f largs g) + |VRTactic res -> res + |_ -> + errorlabstrm "Tacinterp.interp_rec" [<'sTR + "Interpretation gives a non-tactic value">] +(*Interprets a primitive tactic*) +and interp_atomic loc opn args=vernac_tactic(opn,args) +(*Interprets sequences of tactics*) +and interp_semi_list acc lfun lmatch=function + (Node(_,"TACLIST",seq))::l -> + interp_semi_list (tclTHENS acc (List.map (tac_interp lfun lmatch) seq)) + lfun lmatch l + |t::l -> + interp_semi_list (tclTHEN acc (tac_interp lfun lmatch t)) lfun lmatch l + |[] -> acc +(*Interprets bindings for tactics*) +and bind_interp evc env lfun lmatch goalopt=function + Node(_,"BINDING", [Num(_,n);Node(loc,"COMMAND",[c])]) -> + (NoDep n,constr_of_Constr (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt) (Node(loc,"COMMAND",[c]))))) + |Node(_,"BINDING", [Nvar(loc0,s); Node(loc1,"COMMAND",[c])]) -> + (Dep (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) + (Nvar(loc0,s))))),constr_of_Constr (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt) (Node(loc1,"COMMAND",[c]))))) + |Node(_,"BINDING", [Node(loc,"COMMAND",[c])]) -> + (Com,constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) + (Node(loc,"COMMAND",[c]))))) + |x -> + errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding"; + print_ast x>] +(*Interprets a COMMAND expression*) +and com_interp (evc,env,lfun,lmatch,goalopt)=function + Node(_,"EVAL",[c;rtc]) -> + let redexp= + unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) rtc)) + in + VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr1 evc + env (make_subs_list lfun) lmatch c))) + |c -> VArg (Constr (interp_constr1 evc env (make_subs_list lfun) lmatch c)) +(*Interprets a CASTEDCOMMAND expression*) +and cast_com_interp (evc,env,lfun,lmatch,goalopt) com= + match goalopt with + Some gl -> + (match com with + Node(_,"EVAL",[c;rtc]) -> + let redexp= + unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) rtc)) + in + VArg (Constr ((reduction_of_redexp redexp) env evc + (interp_casted_constr1 evc env (make_subs_list lfun) lmatch + c (pf_concl gl)))) + |c -> + VArg (Constr (interp_casted_constr1 evc env (make_subs_list lfun) + lmatch c (pf_concl gl)))) + |None -> + errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">] +and cvt_pattern (evc,env,lfun,lmatch,goalopt)=function + Node(_,"PATTERN", Node(loc,"COMMAND",[com])::nums) -> + let occs=List.map num_of_ast nums + and csr= + constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) + (Node(loc,"COMMAND",[com])))) + in + let jdt=Typing.unsafe_machine env evc csr + in + (occs, jdt.Environ.uj_val, jdt.Environ.uj_type) + |arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern") +and cvt_unfold (evc,env,lfun,lmatch,goalopt)=function + Node(_,"UNFOLD", com::nums) -> + (List.map num_of_ast nums,glob_nvar (id_of_Identifier (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt) com)))) + |arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold") +(*Interprets the arguments of Fold*) +and cvt_fold (evc,env,lfun,lmatch,goalopt)=function + Node(_,"COMMAND",[c]) as ast -> + constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) ast)) + |arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold") +(*Interprets the reduction flags*) +and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf= + let beta = ref false in + let delta = ref false in + let iota = ref false in + let idents = ref (None: (sorts oper -> bool) option) in + let set_flag = function + Node(_,"Beta",[]) -> beta := true + | Node(_,"Delta",[]) -> delta := true + | Node(_,"Iota",[]) -> iota := true + | Node(loc,"Unf",l) -> + if !delta then + if !idents = None then + let idl= + List.map (fun v -> glob_nvar (id_of_Identifier (unvarg + (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l + in + idents := Some + (function + Const sp -> List.mem sp idl + | Abst sp -> List.mem sp idl + | _ -> false) + else user_err_loc(loc,"flag_of_ast", + [< 'sTR"Cannot specify identifiers to unfold twice" >]) + else user_err_loc(loc,"flag_of_ast", + [< 'sTR"Delta must be specified before" >]) + | Node(loc,"UnfBut",l) -> + if !delta then + if !idents = None then + let idl= + List.map (fun v -> glob_nvar (id_of_Identifier (unvarg + (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l + in + idents := Some + (function + Const sp -> not (List.mem sp idl) + | Abst sp -> not (List.mem sp idl) + | _ -> false) + else user_err_loc(loc,"flag_of_ast", + [< 'sTR"Cannot specify identifiers to unfold twice" >]) + else user_err_loc(loc,"flag_of_ast", + [< 'sTR"Delta must be specified before" >]) + | arg -> invalid_arg_loc (Ast.loc arg,"flag_of_ast") + in + List.iter set_flag lf; + { r_beta = !beta; + r_iota = !iota; + r_delta = match (!delta,!idents) with + (false,_) -> (fun _ -> false) + | (true,None) -> (fun _ -> true) + | (true,Some p) -> p } +(*Interprets a reduction expression*) +and redexp_of_ast (evc,env,lfun,lmatch,goalopt)=function + |("Red", []) -> Red + |("Hnf", []) -> Hnf + |("Simpl", []) -> Simpl + |("Unfold", ul) -> + Unfold (List.map (cvt_unfold (evc,env,lfun,lmatch,goalopt)) ul) + |("Fold", cl) -> Fold (List.map (cvt_fold (evc,env,lfun,lmatch,goalopt)) cl) + |("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf) + |("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf) + |("Pattern",lp) -> + Pattern (List.map (cvt_pattern (evc,env,lfun,lmatch,goalopt)) lp) + |(s,_) -> invalid_arg ("malformed reduction-expression: "^s) +(*Interprets the patterns of Intro*) +and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)=function + Node(_,"IDENTIFIER", [Nvar(loc,s)]) -> + IdPat (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) + (Nvar (loc,s))))) + |Node(_,"DISJPATTERN", l) -> + DisjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) + |Node(_,"CONJPATTERN", l) -> + ConjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) + |Node(_,"LISTPATTERN", l) -> + ListPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) + |x -> + errorlabstrm "cvt_intro_pattern" + [<'sTR "Not the expected form for an introduction pattern!";print_ast + x>] +(*Interprets a pattern of Let*) +and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l)=function + Node(_,"HYPPATTERN", Nvar(loc,s)::nums) -> + (o,(id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) + (Nvar (loc,s)))),List.map num_of_ast nums)::l) + |Node(_,"CCLPATTERN", nums) -> + if o<>None then + error "\"Goal\" occurs twice" + else + (Some (List.map num_of_ast nums), l) + |arg -> invalid_arg_loc (Ast.loc arg,"cvt_hyppattern");; + +(*Interprets tactic arguments*) +let interp_tacarg sign ast=unvarg (val_interp sign ast);; + +(*Initial call for interpretation*) +let interp=tac_interp [] [];; -let cvt_bind = function - | Node(_,"BINDING", [Num(_,n); Node(_,"COMMAND",[c])]) -> (NoDep n,c) - | Node(_,"BINDING", [Nvar(_,s); Node(_,"COMMAND",[c])]) -> - let id = id_of_string s in (Dep id,c) - | Node(_,"BINDING", [Node(_,"COMMAND",[c])]) -> (Com,c) - | x -> errorlabstrm "cvt_bind" - [< 'sTR "Not the expected form in binding!"; print_ast x >] - -let rec cvt_intro_pattern = function - | Node(_,"IDENTIFIER", [Nvar(_,s)]) -> IdPat (id_of_string s) - | Node(_,"DISJPATTERN", l) -> DisjPat (List.map cvt_intro_pattern l) - | Node(_,"CONJPATTERN", l) -> ConjPat (List.map cvt_intro_pattern l) - | Node(_,"LISTPATTERN", l) -> ListPat (List.map cvt_intro_pattern l) - | x -> errorlabstrm "cvt_intro_pattern" - [< 'sTR "Not the expected form for an introduction pattern!"; - print_ast x >] - -let cvt_letpattern (o,l) = function - | Node(_,"HYPPATTERN", Nvar(_,s)::nums) -> - (o, (id_of_string s, List.map num_of_ast nums)::l) - | Node(_,"CCLPATTERN", nums) -> - if o<>None then error "\"Goal\" occurs twice" - else (Some (List.map num_of_ast nums), l) - | arg -> - invalid_arg_loc (Ast.loc arg,"cvt_hyppattern") - -let cvt_letpatterns astl = List.fold_left cvt_letpattern (None,[]) astl - -let cvt_arg = function - | Nvar(_,s) -> - Identifier (id_of_string s) - | Str(_,s) -> - Quoted_string s - | Num(_,n) -> - Integer n - | Node(_,"COMMAND",[c]) -> - Command c - | Node(_,"BINDINGS",astl) -> - Bindings (List.map cvt_bind astl) - | Node(_,"REDEXP",[Node(_,redname,args)]) -> - Redexp (redname,args) - | Node(_,"CLAUSE",cl) -> - Clause (List.map (compose id_of_string nvar_of_ast) cl) - | Node(_,"TACTIC",[ast]) -> - Tacexp ast - | Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) -> - Fixexp (id_of_string s,n,c) - | Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) -> - Cofixexp (id_of_string s,c) - | Node(_,"INTROPATTERN", [ast]) -> - Intropattern (cvt_intro_pattern ast) - | Node(_,"LETPATTERNS", astl) -> - let (o,l) = (cvt_letpatterns astl) in Letpatterns (o,l) - | x -> - anomaly_loc (Ast.loc x, "Tacinterp.cvt_bind", - [< 'sTR "Unrecognizable ast node : "; print_ast x >]) - -let rec interp = function - | Node(loc,opn,tl) -> - (match (opn, tl) with - | ("TACTICLIST",_) -> interp_semi_list tclIDTAC tl - | ("DO",[n;tac]) -> tclDO (num_of_ast n) (interp tac) - | ("TRY",[tac]) -> tclTRY (interp tac) - | ("INFO",[tac]) -> tclINFO (interp tac) - | ("REPEAT",[tac]) -> tclREPEAT (interp tac) - | ("ORELSE",[tac1;tac2]) -> tclORELSE (interp tac1) (interp tac2) - | ("FIRST",l) -> tclFIRST (List.map interp l) - | ("TCLSOLVE",l) -> tclSOLVE (List.map interp l) - | ("CALL",macro::args) -> - interp (macro_expand loc (nvar_of_ast macro) - (List.map cvt_arg args)) - | _ -> interp_atomic loc opn (List.map cvt_arg tl)) - | ast -> user_err_loc(Ast.loc ast,"Tacinterp.interp", - [< 'sTR"A non-ASTnode constructor was found" >]) - -and interp_atomic loc opn args = - try - tacinterp_map opn args - with Not_found -> - try - vernac_tactic(opn,args) - with e -> - Stdpp.raise_with_loc loc e - -and interp_semi_list acc = function - | (Node(_,"TACLIST",seq))::l -> - interp_semi_list (tclTHENS acc (List.map interp seq)) l - | t::l -> interp_semi_list (tclTHEN acc (interp t)) l - | [] -> acc - - let is_just_undef_macro ast = match ast with | Node(_,"TACTICLIST",[Node(loc,"CALL",macro::_)]) -> diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 3e913f808a..87d5e2a1ff 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -4,25 +4,42 @@ (*i*) open Pp open Names -open Proof_trees +open Proof_type open Tacmach open Term (*i*) -(* Interpretation of tactics. *) +(*Values for interpretation*) +type value= + VTactic of tactic + |VFTactic of tactic_arg list*(tactic_arg list->tactic) + |VRTactic of (goal list sigma * validation) + |VArg of tactic_arg + |VFun of (string*value) list*string option list*Coqast.t + |VVoid + |VRec of value ref;; -val cvt_arg : Coqast.t -> tactic_arg +(*Gives the constr corresponding to a CONSTR tactic_arg*) +val constr_of_Constr:tactic_arg-> constr;; + +(*Signature for interpretation: val_interp and interpretation functions*) +type interp_sign= + evar_declarations*Environ.env*(string*value) list*(int*constr) list* + goal sigma option;; + +(*Adds a Tactic Definition in the table*) +val add_tacdef : string -> value -> unit;; + +(*Interprets any expression*) +val val_interp:interp_sign->Coqast.t->value;; + +(*Interprets tactic arguments*) +val interp_tacarg:interp_sign->Coqast.t->tactic_arg;; -val tacinterp_add : string * (tactic_arg list -> tactic) -> unit -val tacinterp_map : string -> tactic_arg list -> tactic -val tacinterp_init : unit -> unit val interp : Coqast.t -> tactic -val interp_atomic : Coqast.loc -> string -> tactic_arg list -> tactic -val interp_semi_list : tactic -> Coqast.t list -> tactic val vernac_interp : Coqast.t -> tactic val vernac_interp_atomic : identifier -> tactic_arg list -> tactic -val overwriting_tacinterp_add : string * (tactic_arg list -> tactic) -> unit + val is_just_undef_macro : Coqast.t -> string option val bad_tactic_args : string -> 'a - diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 9191522dc3..5a69ecf577 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -14,24 +14,21 @@ open Evd open Typing open Tacred open Proof_trees +open Proof_type open Logic open Refiner open Evar_refiner - -type 'a sigma = 'a Refiner.sigma - -type validation = proof_tree list -> proof_tree - -type tactic = goal sigma -> (goal list sigma * validation) - let re_sig it gc = { it = it; sigma = gc } - (**************************************************************) (* Operations for handling terms under a local typing context *) (**************************************************************) +type 'a sigma = 'a Proof_type.sigma;; +type validation = Proof_type.validation;; +type tactic = Proof_type.tactic;; + let unpackage = Refiner.unpackage let repackage = Refiner.repackage let apply_sig_tac = Refiner.apply_sig_tac diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 9a946e7620..0baa909c99 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -8,6 +8,7 @@ open Sign open Environ open Reduction open Proof_trees +open Proof_type open Refiner open Evar_refiner open Tacred @@ -15,7 +16,9 @@ open Tacred (* Operations for handling terms under a local typing context. *) -type 'a sigma +type 'a sigma = 'a Proof_type.sigma;; +type validation = Proof_type.validation;; +type tactic = Proof_type.tactic;; val sig_it : 'a sigma -> 'a val sig_sig : goal sigma -> global_constraints @@ -73,8 +76,6 @@ val pf_const_value : goal sigma -> constr -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -type validation = proof_tree list -> proof_tree -type tactic = goal sigma -> (goal list sigma * validation) type transformation_tactic = proof_tree -> (goal list * validation) val frontier : transformation_tactic diff --git a/tactics/Equality.v b/tactics/Equality.v index 66f5252a99..1cbf506270 100644 --- a/tactics/Equality.v +++ b/tactics/Equality.v @@ -84,9 +84,9 @@ Grammar tactic simple_tactic := | rewriteRL [ "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(RewriteRL ($LIST $cl))] | rewrite [ "Rewrite" constrarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))] -| condrewriteLR [ "Conditional" tactic_com($tac) "Rewrite" "->" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))] -| condrewriteRL [ "Conditional" tactic_com($tac) "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(CondRewriteRL (TACTIC $tac) ($LIST $cl))] -| condrewrite [ "Conditional" tactic_com($tac) "Rewrite" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))] +| condrewriteLR [ "Conditional" tactic_expr($tac) "Rewrite" "->" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))] +| condrewriteRL [ "Conditional" tactic_expr($tac) "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(CondRewriteRL (TACTIC $tac) ($LIST $cl))] +| condrewrite [ "Conditional" tactic_expr($tac) "Rewrite" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))] | rewrite_in [ "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ] -> [(RewriteLRin $h ($LIST $cl))] @@ -96,15 +96,15 @@ Grammar tactic simple_tactic := -> [(RewriteRLin $h ($LIST $cl))] | condrewriteLRin - [ "Conditional" tactic_com($tac) "Rewrite" "->" constrarg_binding_list($cl) + [ "Conditional" tactic_expr($tac) "Rewrite" "->" constrarg_binding_list($cl) "in" identarg($h) ] -> [(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))] | condrewriteRLin - [ "Conditional" tactic_com($tac) "Rewrite" "<-" constrarg_binding_list($cl) + [ "Conditional" tactic_expr($tac) "Rewrite" "<-" constrarg_binding_list($cl) "in" identarg($h)] -> [(CondRewriteRLin (TACTIC $tac) $h ($LIST $cl))] | condrewritein - [ "Conditional" tactic_com($tac) "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ] + [ "Conditional" tactic_expr($tac) "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ] -> [(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))] | DRewriteLR [ "Dependent" "Rewrite" "->" identarg($id) ] diff --git a/tactics/auto.ml b/tactics/auto.ml index f0b4e81add..2a98b8e2fb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -13,7 +13,7 @@ open Reduction open Typing open Pattern open Tacmach -open Proof_trees +open Proof_type open Pfedit open Rawterm open Tacred diff --git a/tactics/auto.mli b/tactics/auto.mli index d97e82df63..50460de17a 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -6,7 +6,7 @@ open Util open Names open Term open Sign -open Proof_trees +open Proof_type open Tacmach open Clenv open Pattern diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index a21b3e6d7c..237af5c060 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -111,8 +111,8 @@ open Generic open Term open Environ open Reduction +open Proof_type open Rawterm -open Proof_trees open Tacmach open Tactics open Clenv @@ -279,17 +279,17 @@ let dHyp id gls = destructHyp false id gls open Tacinterp -let _ = - tacinterp_add - ("DHyp",(function - | [Identifier id] -> dHyp id - | _ -> bad_tactic_args "DHyp")) +let _= + add_tactic "DHyp" + (function + | [Identifier id] -> dHyp id + | _ -> bad_tactic_args "DHyp") -let _ = - tacinterp_add - ("CDHyp",(function - | [Identifier id] -> cDHyp id - | _ -> bad_tactic_args "CDHyp")) +let _= + add_tactic "CDHyp" + (function + | [Identifier id] -> cDHyp id + | _ -> bad_tactic_args "CDHyp") (* [DConcl gls] @@ -302,11 +302,11 @@ let dConcl gls = let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in tclFIRST (List.map (applyDestructor None false) sorted_ddl) gls -let _ = - tacinterp_add - ("DConcl",(function - | [] -> dConcl - | _ -> bad_tactic_args "DConcl")) +let _= + add_tactic "DConcl" + (function + | [] -> dConcl + | _ -> bad_tactic_args "DConcl") let to2Lists (table : t) = Nbtermdn.to2lists table diff --git a/tactics/elim.ml b/tactics/elim.ml index 4abff0e4d2..ff07f6c09a 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -7,7 +7,7 @@ open Names open Generic open Term open Reduction -open Proof_trees +open Proof_type open Clenv open Hipattern open Tacmach diff --git a/tactics/elim.mli b/tactics/elim.mli index ee1b10a377..594dc62eaf 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -4,7 +4,7 @@ (*i*) open Names open Term -open Proof_trees +open Proof_type open Tacmach open Tacticals (*i*) diff --git a/tactics/equality.ml b/tactics/equality.ml index b282309927..72f02e7205 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -14,7 +14,7 @@ open Instantiate open Typeops open Typing open Tacmach -open Proof_trees +open Proof_type open Logic open Wcclausenv open Pattern @@ -1936,7 +1936,7 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls = (repackage sigr gl,validation_fun) (*Collects the arguments of AutoRewrite ast node*) -let dyn_autorewrite largs= +(*let dyn_autorewrite largs= let rec explicit_base largs = let tacargs = List.map cvt_arg largs in List.map @@ -2016,8 +2016,7 @@ let dyn_autorewrite largs= anomalylabstrm "dyn_autorewrite" [<'sTR "Bad call of list_args (not a REDEXP)">] in - list_args largs + list_args largs*) (*Adds and hides the AutoRewrite tactic*) -let h_autorewrite = hide_tactic "AutoRewrite" dyn_autorewrite - +(*let h_autorewrite = hide_tactic "AutoRewrite" dyn_autorewrite*) diff --git a/tactics/equality.mli b/tactics/equality.mli index 789328f51b..3341167d86 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -7,7 +7,7 @@ open Term open Sign open Evd open Environ -open Proof_trees +open Proof_type open Tacmach open Hipattern open Pattern diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 049fb1e14b..48b29ea5ed 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -2,7 +2,7 @@ (* $Id$ *) open Term -open Proof_trees +open Proof_type open Tacmach open Tacentries diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 3929903644..183558f601 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -4,7 +4,7 @@ (*i*) open Names open Term -open Proof_trees +open Proof_type open Tacmach open Tacentries (*i*) diff --git a/tactics/inv.ml b/tactics/inv.ml index 53eaa4ad15..8f19a69248 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -13,7 +13,7 @@ open Printer open Reduction open Retyping open Tacmach -open Proof_trees +open Proof_type open Clenv open Tactics open Wcclausenv diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli index 687de4d7d1..bc9e836ab6 100644 --- a/tactics/tacentries.mli +++ b/tactics/tacentries.mli @@ -2,7 +2,7 @@ (* $Id$ *) (*i*) -open Proof_trees +open Proof_type open Tacmach (*i*) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 6e7831b1cb..888785ae92 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -12,7 +12,6 @@ open Reduction open Environ open Declare open Tacmach -open Proof_trees open Clenv open Pattern open Wcclausenv diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 24b705ac72..ae38c210e4 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,7 +6,7 @@ open Names open Term open Sign open Tacmach -open Proof_trees +open Proof_type open Clenv open Reduction open Pattern diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 66dd8b1ad6..b21ac1825b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -16,6 +16,7 @@ open Pfedit open Tacred open Tacmach open Proof_trees +open Proof_type open Logic open Clenv open Tacticals @@ -37,13 +38,6 @@ let get_pairs_from_bindings = | _ -> error "not a binding list!" in List.map pair_from_binding - -let get_commands = - let command_from_tacarg = function - | (Command x) -> x - | _ -> error "get_commands: not a command!" - in - List.map command_from_tacarg let rec string_head_bound = function | DOPN(Const _,_) as x -> @@ -211,9 +205,9 @@ let unfold_option loccname = reduct_option (unfoldn loccname) let pattern_option l = reduct_option (pattern_occs l) let dyn_change = function - | [Command (com); Clause cl] -> + | [Constr c; Clause cl] -> (fun goal -> - let c = Astterm.interp_type (project goal) (pf_env goal) com in +(* let c = Astterm.interp_type (project goal) (pf_env goal) com in*) in_combinator (change_in_concl c) (change_in_hyp c) cl goal) | l -> bad_tactic_args "change" l @@ -224,11 +218,7 @@ let reduce redexp cl goal = redin_combinator (reduction_of_redexp redexp) cl goal let dyn_reduce = function - | [Redexp (redn,args); Clause cl] -> - (fun goal -> - let redexp = - Astterm.redexp_of_ast (project goal) (pf_env goal) (redn,args) in - reduce redexp cl goal) + | [Redexp redexp; Clause cl] -> (fun goal -> reduce redexp cl goal) | l -> bad_tactic_args "reduce" l (* Unfolding occurrences of a constant *) @@ -242,7 +232,7 @@ let unfold_constr c = [< 'sTR "Cannot unfold a non-constant." >] (*******************************************) -(* Introduction tactics *) +(* Introduction tactics *) (*******************************************) let next_global_ident_from id avoid = @@ -603,10 +593,10 @@ let generalize lconstr gl = apply_type newcl lconstr gl let dyn_generalize = - fun argsl -> tactic_com_list generalize (get_commands argsl) + fun argsl -> generalize (List.map Tacinterp.constr_of_Constr argsl) let dyn_generalize_dep = function - | [Command com] -> tactic_com generalize_dep com + | [Constr csr] -> generalize_dep csr | l -> bad_tactic_args "dyn_generalize_dep" l (* Faudra-t-il une version avec plusieurs args de generalize_dep ? diff --git a/tactics/tactics.mli b/tactics/tactics.mli index d36b162adf..6ee8b95481 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -6,7 +6,7 @@ open Names open Term open Environ open Tacmach -open Proof_trees +open Proof_type open Reduction open Evd open Clenv diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli index deae4091ff..01d05a690d 100644 --- a/tactics/wcclausenv.mli +++ b/tactics/wcclausenv.mli @@ -7,7 +7,7 @@ open Term open Sign open Environ open Evd -open Proof_trees +open Proof_type open Tacmach open Clenv (*i*) diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index ab1a4b9e04..7737c48378 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -38,7 +38,7 @@ Hints Resolve diff_true_false : bool v62. Lemma diff_false_true : ~false=true. Goal. -(Red; Intros H; Apply diff_true_false). +Red; Intros H; Apply diff_true_false. Symmetry. Assumption. Save. @@ -52,7 +52,7 @@ Hints Resolve eq_true_false_abs : bool. Lemma not_true_is_false : (b:bool)~b=true->b=false. Destruct b. Intros. -(Red in H; Elim H). +Red in H; Elim H. Reflexivity. Intros abs. Reflexivity. @@ -185,13 +185,13 @@ Save. Lemma negb_orb : (b1,b2:bool) (negb (orb b1 b2)) = (andb (negb b1) (negb b2)). Proof. - (Destruct b1; Destruct b2; Simpl; Reflexivity). + Destruct b1; Destruct b2; Simpl; Reflexivity. Qed. Lemma negb_andb : (b1,b2:bool) (negb (andb b1 b2)) = (orb (negb b1) (negb b2)). Proof. - (Destruct b1; Destruct b2; Simpl; Reflexivity). + Destruct b1; Destruct b2; Simpl; Reflexivity. Qed. Lemma negb_sym : (b,b':bool)(b'=(negb b))->(b=(negb b')). @@ -223,12 +223,12 @@ Save. Lemma orb_prop : (a,b:bool)(orb a b)=true -> (a = true)\/(b = true). -Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool. +Induction a; Induction b; Simpl; Try '(Intro H;Discriminate H); Auto with bool. Save. Lemma orb_prop2 : (a,b:bool)(Is_true (orb a b)) -> (Is_true a)\/(Is_true b). -Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool. +Induction a; Induction b; Simpl; Try '(Intro H;Discriminate H); Auto with bool. Save. Lemma orb_true_intro @@ -306,14 +306,16 @@ Lemma andb_prop : (a,b:bool)(andb a b) = true -> (a = true)/\(b = true). Proof. - Induction a; Induction b; Simpl; Try (Intro H;Discriminate H);Auto with bool. + Induction a; Induction b; Simpl; Try '(Intro H;Discriminate H); + Auto with bool. Save. Hints Resolve andb_prop : bool v62. Lemma andb_prop2 : (a,b:bool)(Is_true (andb a b)) -> (Is_true a)/\(Is_true b). Proof. - Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool. + Induction a; Induction b; Simpl; Try '(Intro H;Discriminate H); + Auto with bool. Save. Hints Resolve andb_prop2 : bool v62. diff --git a/theories/Zarith/Wf_Z.v b/theories/Zarith/Wf_Z.v index 6b015c77f4..2be8bf5c1a 100644 --- a/theories/Zarith/Wf_Z.v +++ b/theories/Zarith/Wf_Z.v @@ -35,7 +35,7 @@ Destruct x; Intros; Apply f_equal with f:=POS; Apply convert_intro; Auto with arith | Absurd `0 <= (NEG p)`; - [ Unfold Zle; Simpl; Do 2 (Unfold not); Auto with arith + [ Unfold Zle; Simpl; Do 2 '(Unfold not); Auto with arith | Assumption] ]. Save. @@ -61,7 +61,7 @@ Destruct x; Intros; Apply f_equal with f:=POS; Apply convert_intro; Auto with arith | Absurd `0 <= (NEG p)`; - [ Unfold Zle; Simpl; Do 2 (Unfold not); Auto with arith + [ Unfold Zle; Simpl; Do 2 '(Unfold not); Auto with arith | Assumption] ]. Save. diff --git a/theories/Zarith/Zmisc.v b/theories/Zarith/Zmisc.v index 28c4cf2084..a9a974f75f 100644 --- a/theories/Zarith/Zmisc.v +++ b/theories/Zarith/Zmisc.v @@ -210,9 +210,9 @@ Proof. Intro z. Case z; [ Left; Compute; Trivial | Intro p; Case p; Intros; - (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) + '(Right; Compute; Exact I) Orelse '(Left; Compute; Exact I) | Intro p; Case p; Intros; - (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) ]. + '(Right; Compute; Exact I) Orelse '(Left; Compute; Exact I) ]. (*** was Realizer Zeven_bool. Repeat Program; Compute; Trivial. @@ -224,9 +224,9 @@ Proof. Intro z. Case z; [ Left; Compute; Trivial | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) + '(Left; Compute; Exact I) Orelse '(Right; Compute; Trivial) | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ]. + '(Left; Compute; Exact I) Orelse '(Right; Compute; Trivial) ]. (*** was Realizer Zeven_bool. Repeat Program; Compute; Trivial. @@ -238,9 +238,9 @@ Proof. Intro z. Case z; [ Right; Compute; Trivial | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) + '(Left; Compute; Exact I) Orelse '(Right; Compute; Trivial) | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ]. + '(Left; Compute; Exact I) Orelse '(Right; Compute; Trivial) ]. (*** was Realizer Zodd_bool. Repeat Program; Compute; Trivial. @@ -281,21 +281,21 @@ Lemma Zeven_div2 : (x:Z) (Zeven x) -> `x = 2*(Zdiv2 x)`. Proof. Destruct x. Auto with arith. -(Destruct p; Auto with arith). -Intros. (Absurd (Zeven (POS (xI p0))); Red; Auto with arith). -Intros. (Absurd (Zeven `1`); Red; Auto with arith). -(Destruct p; Auto with arith). -Intros. (Absurd (Zeven (NEG (xI p0))); Red; Auto with arith). -Intros. (Absurd (Zeven `-1`); Red; Auto with arith). +Destruct p; Auto with arith. +Intros. Absurd (Zeven (POS (xI p0))); Red; Auto with arith. +Intros. Absurd (Zeven `1`); Red; Auto with arith. +Destruct p; Auto with arith. +Intros. Absurd (Zeven (NEG (xI p0))); Red; Auto with arith. +Intros. Absurd (Zeven `-1`); Red; Auto with arith. Save. Lemma Zodd_div2 : (x:Z) `x >= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)+1`. Proof. Destruct x. -Intros. (Absurd (Zodd `0`); Red; Auto with arith). -(Destruct p; Auto with arith). -Intros. (Absurd (Zodd (POS (xO p0))); Red; Auto with arith). -Intros. (Absurd `(NEG p) >= 0`; Red; Auto with arith). +Intros. Absurd (Zodd `0`); Red; Auto with arith. +Destruct p; Auto with arith. +Intros. Absurd (Zodd (POS (xO p0))); Red; Auto with arith. +Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith. Save. Lemma Z_modulo_2 : (x:Z) `x >= 0` -> { y:Z | `x=2*y` }+{ y:Z | `x=2*y+1` }. @@ -344,7 +344,7 @@ Apply rename with x:=`x ?= y`; Intro r; Elim r; Save. Lemma Zcompare_x_x : (x:Z) `x ?= x` = EGAL. -(Intro; Apply Case (Zcompare_EGAL x x) of [h1,h2: ?]h2 end). +Intro; Apply Case (Zcompare_EGAL x x) of [h1,h2: ?]h2 end. Apply refl_equal. Save. diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v index bee3e0a234..e9678721b9 100644 --- a/theories/Zarith/auxiliary.v +++ b/theories/Zarith/auxiliary.v @@ -564,7 +564,7 @@ Theorem OMEGA10:(v,c1,c2,l1,l2,k1,k2:Z) = (Zplus (Zmult v (Zplus (Zmult c1 k1) (Zmult c2 k2))) (Zplus (Zmult l1 k1) (Zmult l2 k2))). -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); +Intros; Repeat '(Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Rewrite (Zplus_permute (Zmult l1 k1) (Zmult (Zmult v c2) k2)); Trivial with arith. Save. @@ -573,7 +573,7 @@ Theorem OMEGA11:(v1,c1,l1,l2,k1:Z) (Zplus (Zmult (Zplus (Zmult v1 c1) l1) k1) l2) = (Zplus (Zmult v1 (Zmult c1 k1)) (Zplus (Zmult l1 k1) l2)). -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); +Intros; Repeat '(Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Trivial with arith. Save. @@ -581,7 +581,7 @@ Theorem OMEGA12:(v2,c2,l1,l2,k2:Z) (Zplus l1 (Zmult (Zplus (Zmult v2 c2) l2) k2)) = (Zplus (Zmult v2 (Zmult c2 k2)) (Zplus l1 (Zmult l2 k2))). -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); +Intros; Repeat '(Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Rewrite Zplus_permute; Trivial with arith. Save. @@ -610,7 +610,7 @@ Theorem OMEGA15:(v,c1,c2,l1,l2,k2:Z) = (Zplus (Zmult v (Zplus c1 (Zmult c2 k2))) (Zplus l1 (Zmult l2 k2))). -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); +Intros; Repeat '(Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Rewrite (Zplus_permute l1 (Zmult (Zmult v c2) k2)); Trivial with arith. Save. @@ -619,7 +619,7 @@ Theorem OMEGA16: (v,c,l,k:Z) (Zmult (Zplus (Zmult v c) l) k) = (Zplus (Zmult v (Zmult c k)) (Zmult l k)). -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); +Intros; Repeat '(Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Trivial with arith. Save. diff --git a/theories/Zarith/fast_integer.v b/theories/Zarith/fast_integer.v index 93b78f9e44..5d955f5eed 100644 --- a/theories/Zarith/fast_integer.v +++ b/theories/Zarith/fast_integer.v @@ -154,14 +154,14 @@ Definition sub_un := [x:positive] Lemma sub_add_one : (x:positive) (sub_un (add_un x)) = x. Proof. -(Induction x; [Idtac | Idtac | Simpl;Auto with arith ]); -(Intros p; Elim p; [Idtac | Idtac | Simpl;Auto with arith ]); -(Simpl; Intros q H1 H2; Case H2; Simpl; Trivial with arith). +'(Induction x; [Idtac | Idtac | Simpl;Auto with arith ]); +'(Intros p; Elim p; [Idtac | Idtac | Simpl;Auto with arith]); +Simpl; Intros q H1 H2; Case H2; Simpl; Trivial with arith. Save. Lemma is_double_moins_un : (x:positive) (add_un (double_moins_un x)) = (xO x). Proof. -(Induction x;Simpl;Auto with arith); (Intros m H;Rewrite H;Trivial with arith). +'(Induction x;Simpl;Auto with arith); Intros m H;Rewrite H;Trivial with arith. Save. Lemma add_sub_one : (x:positive) (x=xH) \/ (add_un (sub_un x)) = x. @@ -258,7 +258,7 @@ Theorem compare_convert1 : ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL. Proof. Induction x;Induction y;Split;Simpl;Auto with arith; - (Discriminate Orelse (Elim (H p0); Auto with arith)). + Discriminate Orelse '(Elim (H p0); Auto with arith). Save. Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y. @@ -303,7 +303,7 @@ Lemma ZLSI: (compare x y EGAL) = INFERIEUR. Proof. Induction x;Induction y;Simpl;Auto with arith; - (Discriminate Orelse Intros H;Discriminate H). + Discriminate Orelse Intros H;Discriminate H. Save. Lemma ZLIS: @@ -311,23 +311,25 @@ Lemma ZLIS: (compare x y EGAL) = SUPERIEUR. Proof. Induction x;Induction y;Simpl;Auto with arith; - (Discriminate Orelse Intros H;Discriminate H). + Discriminate Orelse Intros H;Discriminate H. Save. Lemma ZLII: (x,y:positive) (compare x y INFERIEUR) = INFERIEUR -> (compare x y EGAL) = INFERIEUR \/ x = y. Proof. -(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate); - (Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E;Auto with arith). +'(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate); + Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E; + Auto with arith. Save. Lemma ZLSS: (x,y:positive) (compare x y SUPERIEUR) = SUPERIEUR -> (compare x y EGAL) = SUPERIEUR \/ x = y. Proof. -(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate); - (Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E;Auto with arith). +'(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate); + Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E; + Auto with arith. Save. Theorem compare_convert_INFERIEUR : @@ -521,7 +523,7 @@ Save. Lemma ZL11: (x:positive) (x=xH) \/ ~(x=xH). Proof. -Intros x;Case x;Intros; ((Left;Reflexivity) Orelse (Right;Discriminate)). +Intros x;Case x;Intros; '(Left;Reflexivity) Orelse '(Right;Discriminate). Save. Lemma ZL12: (q:positive) (add_un q) = (add q xH). @@ -537,7 +539,8 @@ Save. Theorem ZL13: (x,y:positive)(add_carry x y) = (add_un (add x y)). Proof. -(Induction x;Induction y;Simpl;Auto with arith); (Intros q H1;Rewrite H;Auto with arith). +'(Induction x;Induction y;Simpl;Auto with arith); Intros q H1;Rewrite H; + Auto with arith. Save. Theorem ZL14: @@ -669,7 +672,7 @@ Definition Op := [r:relation] Lemma ZC4: (x,y:positive) (compare x y EGAL) = (Op (compare y x EGAL)). Proof. -(((Intros x y;Elim (Dcompare (compare y x EGAL));[Idtac | Intros H;Elim H]); +'('('(Intros x y;Elim (Dcompare (compare y x EGAL));[Idtac | Intros H;Elim H]); Intros E;Rewrite E;Simpl); [Apply ZC3 | Apply ZC2 | Apply ZC1 ]); Assumption. Save. @@ -791,8 +794,8 @@ Save. Theorem Zopp_Zplus: (x,y:Z) (Zopp (Zplus x y)) = (Zplus (Zopp x) (Zopp y)). Proof. -(Intros x y;Case x;Case y;Auto with arith); -(Intros p q;Simpl;Case (compare q p EGAL);Auto with arith). +'(Intros x y;Case x;Case y;Auto with arith); +Intros p q;Simpl;Case (compare q p EGAL);Auto with arith. Save. Theorem Zplus_sym: (x,y:Z) (Zplus x y) = (Zplus y x). @@ -800,10 +803,10 @@ Proof. Induction x;Induction y;Simpl;Auto with arith; [ Intros q;Rewrite add_sym;Auto with arith | Intros q; Rewrite (ZC4 q p); - (Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]); + '(Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]); Intros E;Rewrite E;Auto with arith | Intros q; Rewrite (ZC4 q p); - (Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]); + '(Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]); Intros E;Rewrite E;Auto with arith | Intros q;Rewrite add_sym;Auto with arith ]. Save. @@ -837,10 +840,10 @@ Intros x y z';Case z'; [ Auto with arith | Intros z;Simpl; Rewrite add_assoc;Auto with arith | Intros z; Simpl; - (Elim (Dcompare (compare y z EGAL));[Idtac|Intros H;Elim H;Clear H]); + '(Elim (Dcompare (compare y z EGAL));[Idtac|Intros H;Elim H;Clear H]); Intros E0;Rewrite E0; - (Elim (Dcompare (compare (add x y) z EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E1;Rewrite E1; [ + '(Elim (Dcompare (compare (add x y) z EGAL));[Idtac|Intros H;Elim H; + Clear H]);Intros E1;Rewrite E1; [ Absurd (compare (add x y) z EGAL)=EGAL; [ (* Cas 1 *) Rewrite convert_compare_SUPERIEUR; [ Discriminate @@ -1110,10 +1113,10 @@ Theorem weak_Zmult_plus_distr_r: (Zmult (POS x) (Zplus y z)) = (Zplus (Zmult (POS x) y) (Zmult (POS x) z)). Proof. Intros x y' z';Case y';Case z';Auto with arith;Intros y z; - (Simpl; Rewrite times_add_distr; Trivial with arith) + '(Simpl; Rewrite times_add_distr; Trivial with arith) Orelse - (Simpl; (Elim (Dcompare (compare z y EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E0;Rewrite E0; [ + '(Simpl; '(Elim (Dcompare (compare z y EGAL));[Idtac|Intros H;Elim H; + Clear H]);Intros E0;Rewrite E0; [ Rewrite (compare_convert_EGAL z y E0); Rewrite (convert_compare_EGAL (times x y)); Trivial with arith | Cut (compare (times x z) (times x y) EGAL)=INFERIEUR; [ @@ -1163,12 +1166,12 @@ Definition Zcompare := [x,y:Z] Theorem Zcompare_EGAL : (x,y:Z) (Zcompare x y) = EGAL <-> x = y. Proof. Intros x y;Split; [ - Case x;Case y;Simpl;Auto with arith; Try (Intros;Discriminate H); [ + Case x;Case y;Simpl;Auto with arith; Try '(Intros;Discriminate H); [ Intros x' y' H; Rewrite (compare_convert_EGAL y' x' H); Trivial with arith | Intros x' y' H; Rewrite (compare_convert_EGAL y' x'); [ Trivial with arith | Generalize H; Case (compare y' x' EGAL); - (Trivial with arith Orelse (Intros C;Discriminate C))]] + Trivial with arith Orelse '(Intros C;Discriminate C)]] | Intros E;Rewrite E; Case y; [ Trivial with arith | Simpl;Exact convert_compare_EGAL @@ -1179,18 +1182,18 @@ Theorem Zcompare_ANTISYM : (x,y:Z) (Zcompare x y) = SUPERIEUR <-> (Zcompare y x) = INFERIEUR. Proof. Intros x y;Split; [ - Case x;Case y;Simpl;Intros;( - Trivial with arith Orelse Discriminate H Orelse (Apply ZC1; Assumption) Orelse - (Cut (compare p p0 EGAL)=SUPERIEUR; [ + Case x;Case y;Simpl;Intros;'( + Trivial with arith Orelse Discriminate H Orelse '(Apply ZC1; Assumption) Orelse + '(Cut (compare p p0 EGAL)=SUPERIEUR; [ Intros H1;Rewrite H1;Auto with arith | Apply ZC2; Generalize H ; Case (compare p0 p EGAL); - (Trivial with arith Orelse (Intros H2;Discriminate H2))])) -| Case x;Case y;Simpl;Intros;( - Trivial with arith Orelse Discriminate H Orelse (Apply ZC2; Assumption) Orelse - (Cut (compare p0 p EGAL)=INFERIEUR; [ + Trivial with arith Orelse '(Intros H2;Discriminate H2)])) +| Case x;Case y;Simpl;Intros;'( + Trivial with arith Orelse Discriminate H Orelse '(Apply ZC2; Assumption) Orelse + '(Cut (compare p0 p EGAL)=INFERIEUR; [ Intros H1;Rewrite H1;Auto with arith | Apply ZC1; Generalize H ; Case (compare p p0 EGAL); - (Trivial with arith Orelse (Intros H2;Discriminate H2))]))]. + Trivial with arith Orelse '(Intros H2;Discriminate H2)]))]. Save. Theorem le_minus: (i,h:nat) (le (minus i h) i). @@ -1216,8 +1219,8 @@ Save. Theorem Zcompare_Zopp : (x,y:Z) (Zcompare x y) = (Zcompare (Zopp y) (Zopp x)). Proof. -(Intros x y;Case x;Case y;Simpl;Auto with arith); -(Intros;Rewrite <- ZC4;Trivial with arith). +'(Intros x y;Case x;Case y;Simpl;Auto with arith); +Intros;Rewrite <- ZC4;Trivial with arith. Save. Hints Resolve convert_compare_EGAL. @@ -1227,10 +1230,10 @@ Theorem weaken_Zcompare_Zplus_compatible : (Zcompare (Zplus (POS z) x) (Zplus (POS z) y)) = (Zcompare x y)) -> (x,y,z:Z) (Zcompare (Zplus z x) (Zplus z y)) = (Zcompare x y). Proof. -(Intros H x y z;Case x;Case y;Case z;Auto with arith; -Try (Intros; Rewrite Zcompare_Zopp; Do 2 Rewrite Zopp_Zplus; +'(Intros H x y z;Case x;Case y;Case z;Auto with arith; +Try '(Intros; Rewrite Zcompare_Zopp; Do 2 Rewrite Zopp_Zplus; Rewrite Zopp_NEG; Rewrite H; Simpl; Auto with arith)); -Try (Intros; Simpl; Rewrite <- ZC4; Auto with arith). +Try '(Intros; Simpl; Rewrite <- ZC4; Auto with arith). Save. Hints Resolve ZC4. @@ -1241,14 +1244,15 @@ Theorem weak_Zcompare_Zplus_compatible : Proof. Intros x y z;Case x;Case y;Simpl;Auto with arith; [ Intros p;Apply convert_compare_INFERIEUR; Apply ZL17 -| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E;Rewrite E;Auto with arith; Apply convert_compare_SUPERIEUR; - Rewrite true_sub_convert; [ Unfold gt ;Apply ZL16 | Assumption ] -| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E;Auto with arith; Apply convert_compare_SUPERIEUR;Unfold gt; - Apply ZL17 +| Intros p;'(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H; + Clear H]);Intros E;Rewrite E;Auto with arith; + Apply convert_compare_SUPERIEUR; Rewrite true_sub_convert; [ Unfold gt ; + Apply ZL16 | Assumption ] +| Intros p;'(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H; + Clear H]);Intros E;Auto with arith; Apply convert_compare_SUPERIEUR; + Unfold gt;Apply ZL17 | Intros p q; - (Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear H]); + '(Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear H]); Intros E;Rewrite E;[ Rewrite (compare_convert_EGAL q p E); Apply convert_compare_EGAL | Apply convert_compare_INFERIEUR;Do 2 Rewrite convert_add;Apply lt_reg_l; @@ -1256,26 +1260,27 @@ Intros x y z;Case x;Case y;Simpl;Auto with arith; [ | Apply convert_compare_SUPERIEUR;Unfold gt ;Do 2 Rewrite convert_add; Apply lt_reg_l;Exact (compare_convert_SUPERIEUR q p E) ] | Intros p q; - (Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]); + '(Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]); Intros E;Rewrite E;Auto with arith; Apply convert_compare_SUPERIEUR; Rewrite true_sub_convert; [ Unfold gt; Apply lt_trans with m:=(convert z); [Apply ZL16 | Apply ZL17] | Assumption ] -| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E;Rewrite E;Auto with arith; Simpl; Apply convert_compare_INFERIEUR; - Rewrite true_sub_convert;[Apply ZL16|Assumption] +| Intros p;'(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H; + Clear H]);Intros E;Rewrite E;Auto with arith; Simpl; + Apply convert_compare_INFERIEUR;Rewrite true_sub_convert;[Apply ZL16| + Assumption] | Intros p q; - (Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear H]); + '(Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear H]); Intros E;Rewrite E;Auto with arith; Simpl;Apply convert_compare_INFERIEUR; Rewrite true_sub_convert;[ Apply lt_trans with m:=(convert z) ;[Apply ZL16|Apply ZL17] | Assumption] | Intros p q; - (Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear H]); + '(Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear H]); Intros E0;Rewrite E0; - (Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]); + '(Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]); Intros E1;Rewrite E1; - (Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear H]); + '(Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear H]); Intros E2;Rewrite E2;Auto with arith; [ Absurd (compare q p EGAL)=INFERIEUR; [ Rewrite <- (compare_convert_EGAL z q E0); @@ -1408,7 +1413,7 @@ Theorem Zcompare_trans_SUPERIEUR : (Zcompare x z) = SUPERIEUR. Proof. Intros x y z;Case x;Case y;Case z; Simpl; -Try (Intros; Discriminate H Orelse Discriminate H0); +Try '(Intros; Discriminate H Orelse Discriminate H0); Auto with arith; [ Intros p q r H H0;Apply convert_compare_SUPERIEUR; Unfold gt; Apply lt_trans with m:=(convert q); diff --git a/theories/Zarith/zarith_aux.v b/theories/Zarith/zarith_aux.v index 8b8be64acb..94404d6602 100644 --- a/theories/Zarith/zarith_aux.v +++ b/theories/Zarith/zarith_aux.v @@ -11,13 +11,11 @@ Require Arith. Require Export fast_integer. -Tactic Definition ElimCompare [$com1 $com2] := - [ < : tactic : < - Elim (Dcompare (Zcompare $com1 $com2)); [ +Tactic Definition ElimCompare com1 com2:= + Elim (Dcompare (Zcompare com1 com2)); [ Idtac | Intro hidden_auxiliary; Elim hidden_auxiliary; - Clear hidden_auxiliary ] >>]. - + Clear hidden_auxiliary ]. Definition Zlt := [x,y:Z](Zcompare x y) = INFERIEUR. Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR. @@ -57,7 +55,7 @@ Save. Theorem Zle_gt_trans : (n,m,p:Z)(Zle m n)->(Zgt m p)->(Zgt n p). -Unfold Zle Zgt; Intros n m p H1 H2; ElimCompare m n; [ +Unfold Zle Zgt; Intros n m p H1 H2; '(ElimCompare m n); [ Intro E; Elim (Zcompare_EGAL m n); Intros H3 H4;Rewrite <- (H3 E); Assumption | Intro H3; Apply Zcompare_trans_SUPERIEUR with y:=m;[ Elim (Zcompare_ANTISYM n m); Intros H4 H5;Apply H5; Assumption @@ -67,7 +65,7 @@ Save. Theorem Zgt_le_trans : (n,m,p:Z)(Zgt n m)->(Zle p m)->(Zgt n p). -Unfold Zle Zgt ;Intros n m p H1 H2; ElimCompare p m; [ +Unfold Zle Zgt ;Intros n m p H1 H2; '(ElimCompare p m); [ Intros E;Elim (Zcompare_EGAL p m);Intros H3 H4; Rewrite (H3 E); Assumption | Intro H3; Apply Zcompare_trans_SUPERIEUR with y:=m; [ Assumption @@ -119,7 +117,7 @@ Save. Lemma Zle_gt_S : (n,p:Z)(Zle n p)->(Zgt (Zs p) n). -Unfold Zle Zgt ;Intros n p H; ElimCompare n p; [ +Unfold Zle Zgt ;Intros n p H; '(ElimCompare n p); [ Intros H1;Elim (Zcompare_EGAL n p);Intros H2 H3; Rewrite <- H2; [ Exact (Zgt_Sn_n n) | Assumption ] @@ -154,7 +152,7 @@ Theorem Zcompare_et_un: ~(Zcompare x (Zplus y (POS xH)))=INFERIEUR. Intros x y; Split; [ - Intro H; ElimCompare x (Zplus y (POS xH));[ + Intro H; '(ElimCompare x (Zplus y (POS xH)));[ Intro H1; Rewrite H1; Discriminate | Intros H1; Elim SUPERIEUR_POS with 1:=H; Intros h H2; Absurd (gt (convert h) O) /\ (lt (convert h) (S O)); [ @@ -170,7 +168,7 @@ Intros x y; Split; [ Rewrite (Zplus_sym x);Rewrite Zplus_assoc; Rewrite Zplus_inverse_r; Simpl; Exact H1 ]] | Intros H1;Rewrite -> H1;Discriminate ] -| Intros H; ElimCompare x (Zplus y (POS xH)); [ +| Intros H; '(ElimCompare x (Zplus y (POS xH))); [ Intros H1;Elim (Zcompare_EGAL x (Zplus y (POS xH))); Intros H2 H3; Rewrite (H2 H1); Exact (Zgt_Sn_n y) | Intros H1;Absurd (Zcompare x (Zplus y (POS xH)))=INFERIEUR;Assumption @@ -206,7 +204,7 @@ Save. Theorem Zgt_S : (n,m:Z)(Zgt (Zs n) m)->((Zgt n m)\/(<Z>m=n)). -Intros n m H; Unfold Zgt; ElimCompare n m; [ +Intros n m H; Unfold Zgt; '(ElimCompare n m); [ Elim (Zcompare_EGAL n m); Intros H1 H2 H3;Rewrite -> H1;Auto with arith | Intros H1;Absurd (Zcompare m n)=SUPERIEUR; [ Exact (Zgt_S_le m n H) | Elim (Zcompare_ANTISYM m n); Auto with arith ] @@ -339,7 +337,7 @@ Save. Theorem Zle_antisym : (n,m:Z)(Zle n m)->(Zle m n)->(n=m). -Unfold Zle ;Intros n m H1 H2; ElimCompare n m; [ +Unfold Zle ;Intros n m H1 H2; '(ElimCompare n m); [ Elim (Zcompare_EGAL n m);Auto with arith | Intros H3;Absurd (Zcompare m n)=SUPERIEUR; [ Assumption @@ -432,7 +430,7 @@ Save. Theorem Zle_lt_or_eq : (n,m:Z)(Zle n m)->((Zlt n m) \/ n=m). -Unfold Zle Zlt ;Intros n m H; ElimCompare n m; [ +Unfold Zle Zlt ;Intros n m H; '(ElimCompare n m); [ Elim (Zcompare_EGAL n m);Auto with arith | Auto with arith | Intros H';Absurd (Zcompare n m)=SUPERIEUR;Assumption ]. @@ -440,7 +438,7 @@ Save. Theorem Zle_or_lt : (n,m:Z)((Zle n m)\/(Zlt m n)). -Unfold Zle Zlt ;Intros n m; ElimCompare n m; [ +Unfold Zle Zlt ;Intros n m; '(ElimCompare n m); [ Intros E;Rewrite -> E;Left;Discriminate | Intros E;Rewrite -> E;Left;Discriminate | Elim (Zcompare_ANTISYM n m); Auto with arith ]. @@ -478,18 +476,18 @@ Definition Zmin := [n,m:Z] Lemma Zmin_SS : (n,m:Z)((Zs (Zmin n m))=(Zmin (Zs n) (Zs m))). Intros n m;Unfold Zmin; Rewrite (Zcompare_n_S n m); -ElimCompare n m;Intros E;Rewrite E;Auto with arith. +'(ElimCompare n m);Intros E;Rewrite E;Auto with arith. Save. Lemma Zle_min_l : (n,m:Z)(Zle (Zmin n m) n). -Intros n m;Unfold Zmin ; ElimCompare n m;Intros E;Rewrite -> E; +Intros n m;Unfold Zmin ; '(ElimCompare n m);Intros E;Rewrite -> E; [ Apply Zle_n | Apply Zle_n | Apply Zlt_le_weak; Apply Zgt_lt;Exact E ]. Save. Lemma Zle_min_r : (n,m:Z)(Zle (Zmin n m) m). -Intros n m;Unfold Zmin ;ElimCompare n m;Intros E;Rewrite -> E;[ +Intros n m;Unfold Zmin ;'(ElimCompare n m);Intros E;Rewrite -> E;[ Unfold Zle ;Rewrite -> E;Discriminate | Unfold Zle ;Rewrite -> E;Discriminate | Apply Zle_n ]. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e69d537a1a..7737bdc6ce 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -15,6 +15,7 @@ open Reduction open Pfedit open Tacmach open Proof_trees +open Proof_type open Tacred open Library open Libobject @@ -728,10 +729,10 @@ let _ = let typ_opt,red_option = match rest with | [] -> None, None | [VARG_CONSTR t] -> Some t, None - | [VARG_TACTIC_ARG (Redexp(r1,r2))] -> - None, Some (redexp_of_ast Evd.empty (Global.env()) (r1,r2)) - | [VARG_CONSTR t; VARG_TACTIC_ARG (Redexp(r1,r2))] -> - Some t, Some (redexp_of_ast Evd.empty (Global.env()) (r1,r2)) + | [VARG_TACTIC_ARG (Redexp redexp)] -> + None, Some redexp + | [VARG_CONSTR t; VARG_TACTIC_ARG (Redexp redexp)] -> + Some t, Some redexp | _ -> bad_vernac_args "DEFINITION" in let stre,coe,objdef,idcoe = match kind with @@ -807,9 +808,8 @@ let _ = let _ = add "Eval" (function - | VARG_TACTIC_ARG (Redexp (rn,unf)) :: VARG_CONSTR c :: g -> + | VARG_TACTIC_ARG (Redexp redexp) :: VARG_CONSTR c :: g -> let (evmap,sign) = get_evmap_sign (goal_of_args g) in - let redexp = redexp_of_ast evmap sign (rn,unf) in let redfun = print_eval (reduction_of_redexp redexp) sign in fun () -> mSG (redfun (judgment_of_com evmap sign c)) | _ -> bad_vernac_args "Eval") @@ -1196,20 +1196,19 @@ let _ = | _ -> bad_vernac_args "SYNTAX") let _ = - add "TacticDefinition" - (function - | (VARG_IDENTIFIER na) :: (VARG_AST tacexp) :: idl -> - let ids = - List.map - (function - | (VARG_IDENTIFIER id) -> (string_of_id id, Pcoq.ETast) - | _ -> bad_vernac_args "TacticDefinition") - idl - in - fun () -> - let body = Ast.to_act_check_vars ids Pcoq.ETast tacexp in - Macros.add_macro_hint (string_of_id na) (List.map fst ids, body) - | _ -> bad_vernac_args "TacticDefinition") + add "TACDEF" + (let rec tacdef_fun lacc=function + (VARG_IDENTIFIER name)::(VARG_AST tacexp)::tl -> + let ve= + Tacinterp.val_interp (empty,empty_env,[],[],None) tacexp + in + tacdef_fun ((string_of_id name,ve)::lacc) tl + |[] -> + fun () -> + List.iter (fun (name,ve) -> Tacinterp.add_tacdef name ve) lacc + |_ -> bad_vernac_args "TACDEF" + in + tacdef_fun []) let _ = add "INFIX" diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 3329beff53..ea27b4aa67 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -5,7 +5,7 @@ open Pp open Util open Names open Himsg -open Proof_trees +open Proof_type open Tacinterp open Coqast open Ast @@ -95,7 +95,10 @@ let rec cvt_varg ast = | Node(_,"AST",[a]) -> VARG_AST a | Node(_,"ASTLIST",al) -> VARG_ASTLIST al - | Node(_,"TACTIC_ARG",[targ]) -> VARG_TACTIC_ARG (cvt_arg targ) + | Node(_,"TACTIC_ARG",[targ]) -> + let (evc,env)=Pfedit.get_evmap_sign None + in + VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None) targ) | Node(_,"VERNACDYN",[Dynamic (_,d)]) -> VARG_DYN d | _ -> anomaly_loc (Ast.loc ast, "Vernacinterp.cvt_varg", [< 'sTR "Unrecognizable ast node of vernac arg:"; diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 8f10f8004c..0a5ccb9aac 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -3,7 +3,7 @@ (*i*) open Names -open Proof_trees +open Proof_type (*i*) (* Interpretation of vernac phrases. *) |