aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-06-28 14:27:59 +0000
committerGravatar corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-06-28 14:27:59 +0000
commit33a06cfbb9f035000379f7d994aa6ab10e7ffb66 (patch)
tree544cebe28029a65a2e7a78eb6ce4254707455064
parentecead0d68bc8b1359617e274a7aa8d8bee3aeb77 (diff)
more evar stuff
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--.depend209
-rw-r--r--Makefile3
-rw-r--r--parsing/g_tactic.ml46
-rw-r--r--parsing/g_tacticnew.ml411
-rw-r--r--parsing/pptactic.ml10
-rw-r--r--proofs/evar_refiner.ml44
-rw-r--r--proofs/evar_refiner.mli9
-rw-r--r--proofs/tacexpr.ml2
-rw-r--r--tactics/evar_tactics.ml70
-rw-r--r--tactics/evar_tactics.mli22
-rw-r--r--tactics/extratactics.ml411
-rw-r--r--tactics/hiddentac.ml4
-rw-r--r--tactics/hiddentac.mli4
-rw-r--r--tactics/tacinterp.ml14
-rw-r--r--translate/pptacticnew.ml11
15 files changed, 263 insertions, 167 deletions
diff --git a/.depend b/.depend
index 608375a72..7e5f59c71 100644
--- a/.depend
+++ b/.depend
@@ -46,10 +46,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \
kernel/univ.cmi
kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
kernel/names.cmi kernel/term.cmi kernel/univ.cmi
-kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
- kernel/environ.cmi
kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi
+kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
+ kernel/environ.cmi
kernel/names.cmi: lib/pp.cmi lib/predicate.cmi
kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
kernel/univ.cmi
@@ -69,9 +69,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \
kernel/univ.cmi: kernel/names.cmi lib/pp.cmi
lib/bignat.cmi: lib/pp.cmi
lib/pp.cmi: lib/pp_control.cmi
-lib/rtree.cmi: lib/pp.cmi
-lib/system.cmi: lib/pp.cmi
-lib/util.cmi: lib/pp.cmi
library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \
kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \
kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \
@@ -100,6 +97,9 @@ library/library.cmi: library/libnames.cmi library/libobject.cmi \
library/nameops.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi
library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
lib/util.cmi
+lib/rtree.cmi: lib/pp.cmi
+lib/system.cmi: lib/pp.cmi
+lib/util.cmi: lib/pp.cmi
parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \
library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \
lib/util.cmi
@@ -205,8 +205,7 @@ proofs/clenv.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
kernel/term.cmi pretyping/termops.cmi lib/util.cmi
proofs/evar_refiner.cmi: kernel/environ.cmi pretyping/evd.cmi \
kernel/names.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
- proofs/refiner.cmi kernel/sign.cmi proofs/tacexpr.cmo kernel/term.cmi \
- interp/topconstr.cmi
+ proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi interp/topconstr.cmi
proofs/logic.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi
proofs/pfedit.cmi: library/decl_kinds.cmo kernel/entries.cmi \
@@ -252,6 +251,8 @@ tactics/equality.cmi: kernel/environ.cmi pretyping/evd.cmi \
proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \
tactics/tactics.cmi kernel/term.cmi
+tactics/evar_tactics.cmi: kernel/names.cmi pretyping/rawterm.cmi \
+ proofs/tacexpr.cmo proofs/tacmach.cmi kernel/term.cmi
tactics/extraargs.cmi: parsing/pcoq.cmi proofs/proof_type.cmi \
proofs/tacexpr.cmo kernel/term.cmi interp/topconstr.cmi
tactics/extratactics.cmi: interp/genarg.cmi kernel/names.cmi \
@@ -318,11 +319,11 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo
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/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo
toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
library/libnames.cmi kernel/names.cmi kernel/term.cmi \
interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi
toplevel/vernacinterp.cmi: proofs/tacexpr.cmo
+toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo
translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \
parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
@@ -342,9 +343,9 @@ contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi
contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi
contrib/correctness/past.cmi: kernel/names.cmi kernel/term.cmi \
interp/topconstr.cmi lib/util.cmi
-contrib/correctness/pcic.cmi: pretyping/rawterm.cmi
contrib/correctness/pcicenv.cmi: kernel/names.cmi kernel/sign.cmi \
kernel/term.cmi
+contrib/correctness/pcic.cmi: pretyping/rawterm.cmi
contrib/correctness/pdb.cmi: kernel/names.cmi
contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi
contrib/correctness/penv.cmi: library/libnames.cmi kernel/names.cmi \
@@ -473,6 +474,14 @@ ide/config_lexer.cmo: ide/config_parser.cmi lib/util.cmi
ide/config_lexer.cmx: ide/config_parser.cmx lib/util.cmx
ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi
ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi
+ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
+ ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
+ ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi lib/system.cmi \
+ ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi
+ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
+ ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
+ ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx lib/system.cmx \
+ ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi
ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
kernel/declarations.cmi kernel/environ.cmi pretyping/evarutil.cmi \
pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \
@@ -495,14 +504,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
toplevel/vernacentries.cmx toplevel/vernacexpr.cmx ide/coq.cmi
ide/coq_tactics.cmo: ide/coq_tactics.cmi
ide/coq_tactics.cmx: ide/coq_tactics.cmi
-ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
- ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
- ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi lib/system.cmi \
- ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi
-ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
- ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
- ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx lib/system.cmx \
- ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi
ide/find_phrase.cmo: ide/ideutils.cmi
ide/find_phrase.cmx: ide/ideutils.cmx
ide/highlight.cmo: ide/ideutils.cmi
@@ -655,6 +656,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+ kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+ kernel/univ.cmi lib/util.cmi kernel/modops.cmi
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+ kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+ kernel/univ.cmx lib/util.cmx kernel/modops.cmi
kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -663,12 +670,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
- kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
- kernel/univ.cmi lib/util.cmi kernel/modops.cmi
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
- kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
- kernel/univ.cmx lib/util.cmx kernel/modops.cmi
kernel/names.cmo: lib/hashcons.cmi lib/options.cmi lib/pp.cmi \
lib/predicate.cmi lib/util.cmi kernel/names.cmi
kernel/names.cmx: lib/hashcons.cmx lib/options.cmx lib/pp.cmx \
@@ -749,10 +750,10 @@ 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/explore.cmo: lib/explore.cmi
lib/explore.cmx: lib/explore.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/gmap.cmo: lib/gmap.cmi
+lib/gmap.cmx: lib/gmap.cmi
lib/gset.cmo: lib/gset.cmi
lib/gset.cmx: lib/gset.cmi
lib/hashcons.cmo: lib/hashcons.cmi
@@ -761,24 +762,14 @@ lib/heap.cmo: lib/heap.cmi
lib/heap.cmx: lib/heap.cmi
lib/options.cmo: lib/util.cmi lib/options.cmi
lib/options.cmx: lib/util.cmx lib/options.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/pp.cmo: lib/pp_control.cmi lib/pp.cmi
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi
lib/predicate.cmo: lib/predicate.cmi
lib/predicate.cmx: lib/predicate.cmi
lib/profile.cmo: lib/profile.cmi
lib/profile.cmx: lib/profile.cmi
-lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi
-lib/stamps.cmo: lib/stamps.cmi
-lib/stamps.cmx: lib/stamps.cmi
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
-lib/system.cmx: config/coq_config.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: library/decl_kinds.cmo kernel/declarations.cmi \
library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \
library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
@@ -885,6 +876,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
lib/system.cmx library/states.cmi
library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi
library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi
+lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi
+lib/stamps.cmo: lib/stamps.cmi
+lib/stamps.cmx: lib/stamps.cmi
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
+lib/system.cmx: config/coq_config.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/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \
parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
toplevel/vernacexpr.cmo
@@ -1743,6 +1744,16 @@ tactics/equality.cmx: proofs/clenv.cmx interp/coqlib.cmx \
tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
pretyping/termops.cmx kernel/typeops.cmx pretyping/typing.cmx \
kernel/univ.cmx lib/util.cmx toplevel/vernacexpr.cmx tactics/equality.cmi
+tactics/evar_tactics.cmo: proofs/evar_refiner.cmi pretyping/evarutil.cmi \
+ pretyping/evd.cmi proofs/proof_type.cmi proofs/refiner.cmi \
+ kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
+ tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
+ tactics/evar_tactics.cmi
+tactics/evar_tactics.cmx: proofs/evar_refiner.cmx pretyping/evarutil.cmx \
+ pretyping/evd.cmx proofs/proof_type.cmx proofs/refiner.cmx \
+ kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \
+ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
+ tactics/evar_tactics.cmi
tactics/extraargs.cmo: parsing/extend.cmi interp/genarg.cmi \
toplevel/metasyntax.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
tactics/tacinterp.cmi tactics/extraargs.cmi
@@ -1751,31 +1762,31 @@ tactics/extraargs.cmx: parsing/extend.cmx interp/genarg.cmx \
tactics/tacinterp.cmx tactics/extraargs.cmi
tactics/extratactics.cmo: tactics/autorewrite.cmi toplevel/cerrors.cmi \
interp/constrintern.cmi tactics/contradiction.cmi parsing/egrammar.cmi \
- tactics/equality.cmi pretyping/evd.cmi tactics/extraargs.cmi \
- interp/genarg.cmi library/global.cmi tactics/inv.cmi tactics/leminv.cmi \
- library/lib.cmi library/libnames.cmi library/libobject.cmi \
- library/nametab.cmi lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \
- parsing/pptactic.cmi pretyping/rawterm.cmi tactics/refine.cmi \
- proofs/refiner.cmi tactics/setoid_replace.cmi library/summary.cmi \
- proofs/tacexpr.cmo tactics/tacinterp.cmi tactics/tacticals.cmi \
- tactics/tactics.cmi kernel/term.cmi toplevel/vernacinterp.cmi \
- tactics/extratactics.cmi
+ tactics/equality.cmi tactics/evar_tactics.cmi pretyping/evd.cmi \
+ tactics/extraargs.cmi interp/genarg.cmi library/global.cmi \
+ tactics/inv.cmi tactics/leminv.cmi library/lib.cmi library/libnames.cmi \
+ library/libobject.cmi kernel/names.cmi library/nametab.cmi \
+ lib/options.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
+ pretyping/rawterm.cmi tactics/refine.cmi proofs/refiner.cmi \
+ tactics/setoid_replace.cmi library/summary.cmi proofs/tacexpr.cmo \
+ tactics/tacinterp.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+ kernel/term.cmi toplevel/vernacinterp.cmi tactics/extratactics.cmi
tactics/extratactics.cmx: tactics/autorewrite.cmx toplevel/cerrors.cmx \
interp/constrintern.cmx tactics/contradiction.cmx parsing/egrammar.cmx \
- tactics/equality.cmx pretyping/evd.cmx tactics/extraargs.cmx \
- interp/genarg.cmx library/global.cmx tactics/inv.cmx tactics/leminv.cmx \
- library/lib.cmx library/libnames.cmx library/libobject.cmx \
- library/nametab.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \
- parsing/pptactic.cmx pretyping/rawterm.cmx tactics/refine.cmx \
- proofs/refiner.cmx tactics/setoid_replace.cmx library/summary.cmx \
- proofs/tacexpr.cmx tactics/tacinterp.cmx tactics/tacticals.cmx \
- tactics/tactics.cmx kernel/term.cmx toplevel/vernacinterp.cmx \
- tactics/extratactics.cmi
-tactics/hiddentac.cmo: proofs/evar_refiner.cmi interp/genarg.cmi \
+ tactics/equality.cmx tactics/evar_tactics.cmx pretyping/evd.cmx \
+ tactics/extraargs.cmx interp/genarg.cmx library/global.cmx \
+ tactics/inv.cmx tactics/leminv.cmx library/lib.cmx library/libnames.cmx \
+ library/libobject.cmx kernel/names.cmx library/nametab.cmx \
+ lib/options.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
+ pretyping/rawterm.cmx tactics/refine.cmx proofs/refiner.cmx \
+ tactics/setoid_replace.cmx library/summary.cmx proofs/tacexpr.cmx \
+ tactics/tacinterp.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+ kernel/term.cmx toplevel/vernacinterp.cmx tactics/extratactics.cmi
+tactics/hiddentac.cmo: tactics/evar_tactics.cmi interp/genarg.cmi \
proofs/proof_type.cmi pretyping/rawterm.cmi proofs/refiner.cmi \
proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tactics.cmi kernel/term.cmi \
lib/util.cmi tactics/hiddentac.cmi
-tactics/hiddentac.cmx: proofs/evar_refiner.cmx interp/genarg.cmx \
+tactics/hiddentac.cmx: tactics/evar_tactics.cmx interp/genarg.cmx \
proofs/proof_type.cmx pretyping/rawterm.cmx proofs/refiner.cmx \
proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tactics.cmx kernel/term.cmx \
lib/util.cmx tactics/hiddentac.cmi
@@ -2181,20 +2192,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \
toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi
toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi
toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi
-toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \
- parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
- kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
- lib/pp.cmi translate/ppvernacnew.cmi proofs/refiner.cmi \
- library/states.cmi lib/system.cmi tactics/tacinterp.cmi \
- proofs/tacmach.cmi lib/util.cmi toplevel/vernacentries.cmi \
- toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi
-toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
- parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
- kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
- lib/pp.cmx translate/ppvernacnew.cmx proofs/refiner.cmx \
- library/states.cmx lib/system.cmx tactics/tacinterp.cmx \
- proofs/tacmach.cmx lib/util.cmx toplevel/vernacentries.cmx \
- toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi
toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
@@ -2257,6 +2254,20 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \
proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \
toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi
+toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \
+ parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
+ kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+ lib/pp.cmi translate/ppvernacnew.cmi proofs/refiner.cmi \
+ library/states.cmi lib/system.cmi tactics/tacinterp.cmi \
+ proofs/tacmach.cmi lib/util.cmi toplevel/vernacentries.cmi \
+ toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi
+toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
+ parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
+ kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+ lib/pp.cmx translate/ppvernacnew.cmx proofs/refiner.cmx \
+ library/states.cmx lib/system.cmx tactics/tacinterp.cmx \
+ proofs/tacmach.cmx lib/util.cmx toplevel/vernacentries.cmx \
+ toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi
translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \
interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \
pretyping/evd.cmi interp/genarg.cmi library/global.cmi library/lib.cmi \
@@ -2343,6 +2354,12 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx \
tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+ kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \
+ contrib/correctness/pcicenv.cmi
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+ kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \
+ contrib/correctness/pcicenv.cmi
contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \
pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \
kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \
@@ -2357,12 +2374,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \
toplevel/record.cmx kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \
toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi
-contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
- kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \
- contrib/correctness/pcicenv.cmi
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
- kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \
- contrib/correctness/pcicenv.cmi
contrib/correctness/pdb.cmo: interp/constrintern.cmi library/global.cmi \
kernel/names.cmi library/nametab.cmi kernel/term.cmi \
pretyping/termops.cmi contrib/correctness/pdb.cmi
@@ -2520,17 +2531,17 @@ contrib/extraction/extraction.cmo: kernel/declarations.cmi kernel/environ.cmi \
library/libnames.cmi contrib/extraction/miniml.cmi \
contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \
library/nametab.cmi pretyping/recordops.cmi kernel/reduction.cmi \
- pretyping/reductionops.cmi pretyping/retyping.cmi kernel/sign.cmi \
- library/summary.cmi contrib/extraction/table.cmi kernel/term.cmi \
- pretyping/termops.cmi lib/util.cmi contrib/extraction/extraction.cmi
+ pretyping/reductionops.cmi pretyping/retyping.cmi library/summary.cmi \
+ contrib/extraction/table.cmi kernel/term.cmi pretyping/termops.cmi \
+ lib/util.cmi contrib/extraction/extraction.cmi
contrib/extraction/extraction.cmx: kernel/declarations.cmx kernel/environ.cmx \
pretyping/evd.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \
library/libnames.cmx contrib/extraction/miniml.cmi \
contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \
library/nametab.cmx pretyping/recordops.cmx kernel/reduction.cmx \
- pretyping/reductionops.cmx pretyping/retyping.cmx kernel/sign.cmx \
- library/summary.cmx contrib/extraction/table.cmx kernel/term.cmx \
- pretyping/termops.cmx lib/util.cmx contrib/extraction/extraction.cmi
+ pretyping/reductionops.cmx pretyping/retyping.cmx library/summary.cmx \
+ contrib/extraction/table.cmx kernel/term.cmx pretyping/termops.cmx \
+ lib/util.cmx contrib/extraction/extraction.cmi
contrib/extraction/g_extraction.cmo: toplevel/cerrors.cmi \
parsing/egrammar.cmi parsing/extend.cmi \
contrib/extraction/extract_env.cmi interp/genarg.cmi lib/options.cmi \
@@ -2937,6 +2948,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \
proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx \
pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+ parsing/printer.cmi contrib/interface/translate.cmi \
+ contrib/interface/vtp.cmi contrib/interface/xlate.cmi
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+ parsing/printer.cmx contrib/interface/translate.cmx \
+ contrib/interface/vtp.cmx contrib/interface/xlate.cmx
contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \
parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \
pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -2961,14 +2980,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.cmx \
pretyping/termops.cmx contrib/interface/translate.cmx \
pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
contrib/interface/showproof.cmi
-contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
- parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
- parsing/printer.cmi contrib/interface/translate.cmi \
- contrib/interface/vtp.cmi contrib/interface/xlate.cmi
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
- parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
- parsing/printer.cmx contrib/interface/translate.cmx \
- contrib/interface/vtp.cmx contrib/interface/xlate.cmx
contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
interp/constrextern.cmi contrib/interface/ctast.cmo kernel/environ.cmi \
pretyping/evarutil.cmi pretyping/evd.cmi library/libobject.cmi \
@@ -3151,12 +3162,12 @@ contrib/romega/refl_omega.cmx: contrib/romega/const_omega.cmx \
proofs/logic.cmx kernel/names.cmx contrib/romega/omega2.cmx \
lib/options.cmx lib/pp.cmx parsing/printer.cmx proofs/tacmach.cmx \
tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx
-contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi
-contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx
contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \
kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi
contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \
kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx
+contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi
+contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx
contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo kernel/declarations.cmi \
library/declare.cmi library/dischargedhypsmap.cmi \
contrib/xml/doubleTypeInference.cmi kernel/environ.cmi \
@@ -3219,8 +3230,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \
contrib/xml/unshare.cmx lib/util.cmx contrib/xml/xml.cmx
contrib/xml/unshare.cmo: contrib/xml/unshare.cmi
contrib/xml/unshare.cmx: contrib/xml/unshare.cmi
-contrib/xml/xml.cmo: contrib/xml/xml.cmi
-contrib/xml/xml.cmx: contrib/xml/xml.cmi
contrib/xml/xmlcommand.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \
contrib/xml/cic2acic.cmo config/coq_config.cmi library/decl_kinds.cmo \
kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
@@ -3247,10 +3256,8 @@ contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
lib/util.cmx toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx
-ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
- ide/utils/configwin_types.cmo ide/utils/configwin.cmi
-ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
- ide/utils/configwin_types.cmx ide/utils/configwin.cmi
+contrib/xml/xml.cmo: contrib/xml/xml.cmi
+contrib/xml/xml.cmx: contrib/xml/xml.cmi
ide/utils/configwin_html_config.cmo: ide/utils/configwin_ihm.cmo \
ide/utils/configwin_messages.cmo ide/utils/configwin_types.cmo \
ide/utils/uoptions.cmi
@@ -3261,6 +3268,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/configwin_messages.cmo \
ide/utils/configwin_types.cmo ide/utils/okey.cmi ide/utils/uoptions.cmi
ide/utils/configwin_ihm.cmx: ide/utils/configwin_messages.cmx \
ide/utils/configwin_types.cmx ide/utils/okey.cmx ide/utils/uoptions.cmx
+ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
+ ide/utils/configwin_types.cmo ide/utils/configwin.cmi
+ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
+ ide/utils/configwin_types.cmx ide/utils/configwin.cmi
ide/utils/configwin_types.cmo: ide/utils/configwin_keys.cmo \
ide/utils/uoptions.cmi
ide/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \
diff --git a/Makefile b/Makefile
index af9eb3af1..56a6bd578 100644
--- a/Makefile
+++ b/Makefile
@@ -181,11 +181,12 @@ TACTICS=\
tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
tactics/nbtermdn.cmo tactics/tacticals.cmo \
tactics/hipattern.cmo tactics/tactics.cmo \
+ tactics/evar_tactics.cmo \
tactics/hiddentac.cmo tactics/elim.cmo \
tactics/dhyp.cmo tactics/auto.cmo \
tactics/setoid_replace.cmo tactics/equality.cmo \
tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \
- tactics/tacinterp.cmo \
+ tactics/tacinterp.cmo
TOPLEVEL=\
toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ae9fc2aed..22a1fc2df 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -303,8 +303,10 @@ GEXTEND Gram
| IDENT "Generalize"; IDENT "Dependent"; c = constr -> TacGeneralizeDep c
| IDENT "LetTac"; (_,na) = name; ":="; c = constr; p = clause_pattern
-> TacLetTac (na,c,p)
- | IDENT "Instantiate"; n = natural; c = constr; cls = clause ->
- TacInstantiate (n,c,cls)
+ | IDENT "Instantiate"; n = natural; c = constr ->
+ TacInstantiate (n,c,ConclLocation ())
+ | IDENT "Instantiate"; n = natural; c = constr; "in"; id = id_or_meta ->
+ TacInstantiate (n,c,HypLocation(id,InHypTypeOnly))
| IDENT "Specialize"; n = OPT natural; lcb = constr_with_bindings ->
TacSpecialize (n,lcb)
| IDENT "LApply"; c = constr -> TacLApply c
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index e307f96f9..16811ff85 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -347,10 +347,13 @@ GEXTEND Gram
p = clause -> TacLetTac (Names.Name id,c,p)
| IDENT "set"; c = constr; p = clause ->
TacLetTac (Names.Anonymous,c,p)
- | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")";
- cls = clause ->
- TacInstantiate (n,c,cls)
-
+ | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")"; "in";
+ hid = hypident ->
+ let (id,(hloc,_)) = hid in
+ TacInstantiate (n,c,HypLocation (id,hloc))
+ | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")" ->
+ TacInstantiate (n,c,ConclLocation ())
+
| IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
TacSpecialize (n,lcb)
| IDENT "lapply"; c = constr -> TacLApply c
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index cd31b7f26..f334dd633 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -154,7 +154,6 @@ let pr_clause pr_id = function
| [] -> mt ()
| l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
-
let pr_clauses pr_id cls =
match cls with
{ onhyps = Some l; onconcl = false } ->
@@ -497,9 +496,12 @@ and pr_atom1 = function
| _ -> pr_clauses pr_ident cl in
hov 1 (str "LetTac" ++ spc () ++ pr_name na ++ str ":=" ++
pr_constr c ++ pcl)
- | TacInstantiate (n,c,cls) ->
- hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++
- pr_clauses pr_ident cls)
+ | TacInstantiate (n,c,ConclLocation ()) ->
+ hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c )
+ | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+ hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++
+ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
+
(* Derived basic tactics *)
| TacSimpleInduction (h,_) ->
hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 18bb5f24f..b04691d87 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -133,7 +133,7 @@ let w_Define sp c wc =
(* w_tactic pour instantiate *)
-let build_open_instance ev rawc wc =
+let w_refine ev rawc wc =
if Evd.is_defined wc.sigma ev then
error "Instantiate called on already-defined evar";
let e_info = Evd.map wc.sigma ev in
@@ -143,43 +143,9 @@ let build_open_instance ev rawc wc =
(Some e_info.evar_concl) rawc in
w_Define ev typed_c {wc with sigma=evd}
-(* The instantiate tactic *)
+(* the instantiate tactic was moved to tactics/evar_tactics.ml *)
-let evars_of evc c =
- let rec evrec acc c =
- match kind_of_term c with
- | Evar (n, _) when Evd.in_dom evc n -> c :: acc
- | _ -> fold_constr evrec acc c
- in
- evrec [] c
-
-let instantiate n rawc ido gl =
- let wc = Refiner.project_with_focus gl in
- let evl =
- match ido with
- None -> evars_of wc.sigma gl.it.evar_concl
- | Some (id,_,_) ->
- let (_,_,typ)=Sign.lookup_named id gl.it.evar_hyps in
- evars_of wc.sigma typ in
- if List.length evl < n then error "not enough evars";
- let ev,_ = destEvar (List.nth evl (n-1)) in
- let wc' = build_open_instance ev rawc wc in
- tclIDTAC {it = gl.it ; sigma = wc'.sigma}
-
-let pfic gls c =
- let evc = gls.sigma in
- Constrintern.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c
-
-(*
-let instantiate_tac = function
- | [Integer n; Command com] ->
- (fun gl -> instantiate n (pfic gl com) gl)
- | [Integer n; Constr c] ->
- (fun gl -> instantiate n c gl)
- | _ -> invalid_arg "Instantiate called with bad arguments"
-*)
-
-(* vernac command existential *)
+(* vernac command Existential *)
let instantiate_pf_com n com pfts =
let gls = top_goal_of_pftreestate pfts in
@@ -194,8 +160,6 @@ let instantiate_pf_com n com pfts =
let e_info = Evd.map sigma sp in
let env = Evarutil.evar_env e_info in
let rawc = Constrintern.interp_rawconstr sigma env com in
- let wc' = build_open_instance sp rawc wc in
+ let wc' = w_refine sp rawc wc in
let newgc = (w_Underlying wc') in
change_constraints_pftreestate newgc pfts
-
-
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 55f5b96c2..2b5fbde42 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -50,9 +50,8 @@ val w_conv_x : wc -> constr -> constr -> bool
val w_const_value : wc -> constant -> constr
val w_defined_evar : wc -> existential_key -> bool
-val instantiate : int -> Rawterm.rawconstr ->
- identifier Tacexpr.gsimple_clause -> tactic
-(*
-val instantiate_tac : tactic_arg list -> tactic
-*)
+val w_refine : evar -> Rawterm.rawconstr -> w_tactic
+
val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate
+
+(* the instantiate tactic was moved to tactics/evar_tactics.ml *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b8c2636c0..e6e0c470b 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -127,7 +127,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacGeneralize of 'constr list
| TacGeneralizeDep of 'constr
| TacLetTac of name * 'constr * 'id gclause
- | TacInstantiate of int * 'constr * 'id gclause
+ | TacInstantiate of int * 'constr * (('id * hyp_location_flag,unit) location)
(* Derived basic tactics *)
| TacSimpleInduction of (quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref)
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
new file mode 100644
index 000000000..7efa9299e
--- /dev/null
+++ b/tactics/evar_tactics.ml
@@ -0,0 +1,70 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Term
+open Util
+open Evar_refiner
+open Tacmach
+open Tacexpr
+open Proof_type
+open Evd
+
+(* The instantiate tactic *)
+
+let evars_of evc c =
+ let rec evrec acc c =
+ match kind_of_term c with
+ | Evar (n, _) when Evd.in_dom evc n -> c :: acc
+ | _ -> fold_constr evrec acc c
+ in
+ evrec [] c
+let instantiate n rawc ido gl =
+ let wc = Refiner.project_with_focus gl in
+ let evl =
+ match ido with
+ ConclLocation () -> evars_of wc.sigma gl.it.evar_concl
+ | HypLocation (id,hloc) ->
+ let decl = Sign.lookup_named id gl.it.evar_hyps in
+ match hloc with
+ InHyp ->
+ (match decl with
+ (_,None,typ) -> evars_of wc.sigma typ
+ | _ -> error
+ "please be more specific : in type or value ?")
+ | InHypTypeOnly ->
+ let (_, _, typ) = decl in evars_of wc.sigma typ
+ | InHypValueOnly ->
+ (match decl with
+ (_,Some body,_) -> evars_of wc.sigma body
+ | _ -> error "not a let .. in hypothesis") in
+ if List.length evl < n then error "not enough uninstantiated evars";
+ let ev,_ = destEvar (List.nth evl (n-1)) in
+ let wc' = w_refine ev rawc wc in
+ Tacticals.tclIDTAC {gl with sigma = wc'.sigma}
+
+(*
+let pfic gls c =
+ let evc = gls.sigma in
+ Constrintern.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c
+
+let instantiate_tac = function
+ | [Integer n; Command com] ->
+ (fun gl -> instantiate n (pfic gl com) gl)
+ | [Integer n; Constr c] ->
+ (fun gl -> instantiate n c gl)
+ | _ -> invalid_arg "Instantiate called with bad arguments"
+*)
+
+let let_evar nam typ gls =
+ let wc = Refiner.project_with_focus gls in
+ let sp = Evarutil.new_evar () in
+ let wc' = w_Declare sp typ wc in
+ let ngls = {gls with sigma = wc'.sigma} in
+ Tactics.forward true nam (mkEvar(sp,[||])) ngls
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
new file mode 100644
index 000000000..df3da392c
--- /dev/null
+++ b/tactics/evar_tactics.mli
@@ -0,0 +1,22 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Tacmach
+open Names
+open Tacexpr
+
+val instantiate : int -> Rawterm.rawconstr ->
+ (identifier * hyp_location_flag, unit) location -> tactic
+
+(*
+val instantiate_tac : tactic_arg list -> tactic
+*)
+
+val let_evar : name -> Term.types -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index daf3bb465..e55df2bf1 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -231,6 +231,17 @@ TACTIC EXTEND Subst
| [ "Subst" ] -> [ subst_all ]
END
+open Evar_tactics
+
+(* evar creation *)
+
+TACTIC EXTEND Evar
+ [ "Evar" "(" ident(id) ":" constr(typ) ")" ] ->
+ [ let_evar (Names.Name id) typ ]
+| [ "Evar" constr(typ) ] ->
+ [ let_evar Names.Anonymous typ ]
+END
+
(** Nijmegen "step" tactic for setoid rewriting *)
open Tacticals
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 21f7d43fc..8afdae999 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -47,8 +47,8 @@ let h_generalize cl = abstract_tactic (TacGeneralize cl) (generalize cl)
let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c)
let h_let_tac na c cl =
abstract_tactic (TacLetTac (na,c,cl)) (letin_tac true na c cl)
-let h_instantiate n c cls =
-(Evar_refiner.instantiate n c (simple_clause_of cls))
+let h_instantiate n c ido =
+(Evar_tactics.instantiate n c ido)
(* abstract_tactic (TacInstantiate (n,c,cls))
(Evar_refiner.instantiate n c (simple_clause_of cls)) *)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 90a2d1b3c..f03e4b755 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -50,8 +50,8 @@ val h_generalize : constr list -> tactic
val h_generalize_dep : constr -> tactic
val h_forward : bool -> name -> constr -> tactic
val h_let_tac : name -> constr -> Tacticals.clause -> tactic
-val h_instantiate : int -> Rawterm.rawconstr ->
- Tacticals.clause -> tactic
+val h_instantiate : int -> Rawterm.rawconstr ->
+ (identifier * hyp_location_flag, unit) location -> tactic
(* Derived basic tactics *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3c2e05f0a..2b2f39e1e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -663,9 +663,12 @@ let rec intern_atomic lf ist x =
let na = intern_name lf ist na in
TacLetTac (na,intern_constr ist c,
(clause_app (intern_hyp_location ist) cls))
- | TacInstantiate (n,c,cls) ->
+ | TacInstantiate (n,c,idh) ->
TacInstantiate (n,intern_constr ist c,
- (clause_app (intern_hyp_location ist) cls))
+ (match idh with
+ ConclLocation () -> ConclLocation ()
+ | HypLocation (id,hloc) ->
+ HypLocation(intern_hyp_or_metaid ist id,hloc)))
(* Automation tactics *)
| TacTrivial l -> TacTrivial l
@@ -1714,9 +1717,12 @@ and interp_atomic ist gl = function
| TacLetTac (na,c,clp) ->
let clp = interp_clause ist gl clp in
h_let_tac (interp_name ist na) (pf_interp_constr ist gl c) clp
- | TacInstantiate (n,c,ido) -> h_instantiate n (fst c)
+ | TacInstantiate (n,c,idh) -> h_instantiate n (fst c)
(* pf_interp_constr ist gl c *)
- (clause_app (interp_hyp_location ist gl) ido)
+ (match idh with
+ ConclLocation () -> ConclLocation ()
+ | HypLocation (id,hloc) ->
+ HypLocation(interp_hyp ist gl id,hloc))
(* Automation tactics *)
| TacTrivial l -> Auto.h_trivial l
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 90c0145e8..23092a733 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -539,11 +539,16 @@ and pr_atom1 env = function
hov 1 (str"(" ++ pr_id id ++ str " :=" ++
pr_lconstrarg env c ++ str")") ++
pr_clauses pr_ident cl)
- | TacInstantiate (n,c,cls) ->
+ | TacInstantiate (n,c,ConclLocation ()) ->
hov 1 (str "instantiate" ++ spc() ++
hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
- pr_lconstrarg env c ++ str ")" ++
- pr_clauses pr_ident cls))
+ pr_lconstrarg env c ++ str ")" ))
+ | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+ hov 1 (str "instantiate" ++ spc() ++
+ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+ pr_lconstrarg env c ++ str ")" )
+ ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
+
(* Derived basic tactics *)
| TacSimpleInduction (h,l) ->
if List.exists (fun (pp,_) -> !pp) !l then
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 11:03:19 +0000