aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-06-29 15:55:40 +0000
committerGravatar corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-06-29 15:55:40 +0000
commitf68638477459eef68fb69adee244f58894e1f0a4 (patch)
tree5555b399af00f9cdb5e91ccb291269af8c5afc19
parent5a9ee53ca774a8878fd37812c114d82779657b16 (diff)
moved instantiate binding to extratactics
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--.depend159
-rw-r--r--contrib/interface/xlate.ml4
-rw-r--r--parsing/argextend.ml446
-rw-r--r--parsing/g_tactic.ml44
-rw-r--r--parsing/g_tacticnew.ml44
-rw-r--r--parsing/pptactic.ml4
-rw-r--r--proofs/tacexpr.ml2
-rw-r--r--tactics/evar_tactics.ml1
-rw-r--r--tactics/extraargs.ml480
-rw-r--r--tactics/extraargs.mli16
-rw-r--r--tactics/extratactics.ml48
-rw-r--r--tactics/tacinterp.ml13
-rw-r--r--tactics/tacinterp.mli12
-rw-r--r--translate/pptacticnew.ml4
14 files changed, 239 insertions, 118 deletions
diff --git a/.depend b/.depend
index bf85f9dd9..f70906fe1 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
@@ -253,8 +253,9 @@ tactics/equality.cmi: kernel/environ.cmi pretyping/evd.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/extraargs.cmi: kernel/names.cmi parsing/pcoq.cmi \
+ proofs/proof_type.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \
+ kernel/term.cmi interp/topconstr.cmi lib/util.cmi
tactics/extratactics.cmi: interp/genarg.cmi kernel/names.cmi \
proofs/proof_type.cmi pretyping/rawterm.cmi kernel/term.cmi
tactics/hiddentac.cmi: interp/genarg.cmi kernel/names.cmi \
@@ -319,11 +320,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 \
@@ -343,9 +344,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 \
@@ -474,6 +475,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 \
@@ -496,14 +505,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
@@ -656,6 +657,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 \
@@ -664,12 +671,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 \
@@ -750,10 +751,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
@@ -762,24 +763,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 \
@@ -886,6 +877,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
@@ -1755,11 +1756,15 @@ tactics/evar_tactics.cmx: proofs/evar_refiner.cmx pretyping/evarutil.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
+ toplevel/metasyntax.cmi library/nameops.cmi kernel/names.cmi \
+ parsing/pcoq.cmi lib/pp.cmi parsing/ppconstr.cmi parsing/pptactic.cmi \
+ proofs/tacexpr.cmo tactics/tacinterp.cmi lib/util.cmi \
+ tactics/extraargs.cmi
tactics/extraargs.cmx: parsing/extend.cmx interp/genarg.cmx \
- toplevel/metasyntax.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
- tactics/tacinterp.cmx tactics/extraargs.cmi
+ toplevel/metasyntax.cmx library/nameops.cmx kernel/names.cmx \
+ parsing/pcoq.cmx lib/pp.cmx parsing/ppconstr.cmx parsing/pptactic.cmx \
+ proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.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 tactics/evar_tactics.cmi pretyping/evd.cmi \
@@ -2192,20 +2197,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 \
@@ -2268,6 +2259,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 \
@@ -2354,6 +2359,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 \
@@ -2368,12 +2379,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
@@ -2948,6 +2953,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 \
@@ -2972,14 +2985,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 \
@@ -3162,12 +3167,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 \
@@ -3230,8 +3235,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 \
@@ -3258,10 +3261,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
@@ -3272,6 +3273,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/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c772382e9..ce44196d8 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1150,9 +1150,9 @@ and xlate_tac =
CT_new_induction
(xlate_int_or_constr a, xlate_using b,
xlate_intro_patt_opt c)
- | TacInstantiate (a, b, cl) ->
+ (*| TacInstantiate (a, b, cl) ->
CT_instantiate(CT_int a, xlate_formula b,
- assert false)
+ assert false) *)
| TacLetTac (na, c, cl) ->
CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c,
(* TODO LATER: This should be shared with Unfold,
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 21f5a7368..126e35663 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -111,21 +111,31 @@ let make_rule loc (prods,act) =
<:expr< ($mlexpr_of_list (fun x -> x) symbs$,$make_act loc act pil$) >>
let declare_tactic_argument for_v8 loc s typ pr f g h rawtyppr globtyppr cl =
- let interp = match f with
- | None -> <:expr< Tacinterp.interp_genarg >>
- | Some f -> <:expr< $lid:f$>> in
- let glob = match g with
- | None -> <:expr< Tacinterp.intern_genarg >>
- | Some f -> <:expr< $lid:f$>> in
- let substitute = match h with
- | None -> <:expr< Tacinterp.subst_genarg >>
- | Some f -> <:expr< $lid:f$>> in
let rawtyp, rawpr = match rawtyppr with
| None -> typ,pr
| Some (t,p) -> t,p in
let globtyp, globpr = match globtyppr with
| None -> typ,pr
| Some (t,p) -> t,p in
+ let glob = match g with
+ | None ->
+ <:expr< fun e x ->
+ out_gen $make_globwit loc typ$
+ (Tacinterp.intern_genarg e
+ (in_gen $make_rawwit loc rawtyp$ x)) >>
+ | Some f -> <:expr< $lid:f$>> in
+ let interp = match f with
+ | None ->
+ <:expr< fun ist gl x ->
+ out_gen $make_wit loc typ$
+ (Tacinterp.interp_genarg ist gl (in_gen $make_globwit loc globtyp$ x)) >>
+ | Some f -> <:expr< $lid:f$>> in
+ let substitute = match h with
+ | None ->
+ <:expr< fun s x ->
+ out_gen $make_globwit loc globtyp$
+ (Tacinterp.subst_genarg s (in_gen $make_globwit loc globtyp$ x)) >>
+ | Some f -> <:expr< $lid:f$>> in
let se = mlexpr_of_string s in
let wit = <:expr< $lid:"wit_"^s$ >> in
let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
@@ -138,23 +148,11 @@ let declare_tactic_argument for_v8 loc s typ pr f g h rawtyppr globtyppr cl =
value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$;
Tacinterp.add_interp_genarg $se$
((fun e x ->
- (in_gen $globwit$
- (out_gen $make_globwit loc typ$
- ($glob$ e
- (in_gen $make_rawwit loc rawtyp$
- (out_gen $rawwit$ x)))))),
+ (in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))),
(fun ist gl x ->
- (in_gen $wit$
- (out_gen $make_wit loc typ$
- ($interp$ ist gl
- (in_gen $make_globwit loc rawtyp$
- (out_gen $globwit$ x)))))),
+ (in_gen $wit$ ($interp$ ist gl (out_gen $globwit$ x)))),
(fun subst x ->
- (in_gen $globwit$
- (out_gen $make_globwit loc typ$
- ($substitute$ subst
- (in_gen $make_globwit loc rawtyp$
- (out_gen $globwit$ x)))))));
+ (in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x)))));
Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None
[(None, None, $rules$)];
Pptactic.declare_extra_genarg_pprule
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 22a1fc2df..db11026a4 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -303,10 +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 ->
+(* | 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))
+ 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 16811ff85..ae052f462 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -347,12 +347,12 @@ 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; ")"; "in";
+ (* | 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 ())
+ TacInstantiate (n,c,ConclLocation ()) *)
| IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
TacSpecialize (n,lcb)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index f334dd633..36440088c 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -496,12 +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,ConclLocation ()) ->
+ (* | 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/tacexpr.ml b/proofs/tacexpr.ml
index e6e0c470b..4c85bf33a 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 * hyp_location_flag,unit) location)
+(* | 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
index 7efa9299e..140deb3a9 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -25,6 +25,7 @@ let evars_of evc c =
| _ -> fold_constr evrec acc c
in
evrec [] c
+
let instantiate n rawc ido gl =
let wc = Refiner.project_with_focus gl in
let evl =
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 4aace33dc..3fbd27c60 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -13,6 +13,9 @@
open Pp
open Pcoq
open Genarg
+open Names
+open Tacexpr
+open Tacinterp
(* Rewriting orientation *)
@@ -23,9 +26,86 @@ let pr_orient _prc _prt = function
| true -> Pp.mt ()
| false -> Pp.str " <-"
+
ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
| [ "->" ] -> [ true ]
| [ "<-" ] -> [ false ]
| [ ] -> [ true ]
END
+
+let pr_gen prc _ c = prc c
+
+let pr_rawc _ _ raw = Ppconstr.pr_rawconstr raw
+
+let interp_raw _ _ (t,_) = t
+
+let glob_raw ist a = Tacinterp.intern_constr ist a
+
+let subst_raw subst arawc = Tacinterp.subst_rawconstr subst arawc
+
+ARGUMENT EXTEND raw
+ TYPED AS rawconstr
+ PRINTED BY pr_rawc
+
+ INTERPRETED BY interp_raw
+ GLOBALIZED BY glob_raw
+ SUBSTITUTED BY subst_raw
+
+ RAW_TYPED AS constr_expr
+ RAW_PRINTED BY pr_gen
+
+ GLOB_TYPED AS rawconstr_and_expr
+ GLOB_PRINTED BY pr_gen
+
+ [ constr(c) ] -> [ c ]
+
+END
+
+type 'id gen_place= ('id * hyp_location_flag,unit) location
+
+type loc_place = identifier Util.located gen_place
+type place = identifier gen_place
+
+let pr_gen_place pr_id = function
+ ConclLocation () -> Pp.mt ()
+ | HypLocation (id,InHyp) -> str "in " ++ pr_id id
+ | HypLocation (id,InHypTypeOnly) ->
+ str "in (Type of " ++ pr_id id ++ str ")"
+ | HypLocation (id,InHypValueOnly) ->
+ str "in (Value of " ++ pr_id id ++ str ")"
+
+let pr_loc_place _ _ = pr_gen_place (fun (_,id) -> Nameops.pr_id id)
+let pr_place _ _ = pr_gen_place Nameops.pr_id
+
+let intern_place ist = function
+ ConclLocation () -> ConclLocation ()
+ | HypLocation (id,hl) -> HypLocation (intern_hyp ist id,hl)
+
+let interp_place ist gl = function
+ ConclLocation () -> ConclLocation ()
+ | HypLocation (id,hl) -> HypLocation (interp_hyp ist gl id,hl)
+
+let subst_place subst pl = pl
+
+ARGUMENT EXTEND hloc
+ TYPED AS place
+ PRINTED BY pr_place
+ INTERPRETED BY interp_place
+ GLOBALIZED BY intern_place
+ SUBSTITUTED BY subst_place
+ RAW_TYPED AS loc_place
+ RAW_PRINTED BY pr_loc_place
+ GLOB_TYPED AS loc_place
+ GLOB_PRINTED BY pr_loc_place
+ [ ] ->
+ [ ConclLocation () ]
+| [ "in" ident(id) ] ->
+ [ HypLocation ((Util.dummy_loc,id),InHyp) ]
+| [ "in" "(" "Type" "of" ident(id) ")" ] ->
+ [ HypLocation ((Util.dummy_loc,id),InHypTypeOnly) ]
+| [ "in" "(" "Value" "of" ident(id) ")" ] ->
+ [ HypLocation ((Util.dummy_loc,id),InHypValueOnly) ]
+
+ END
+
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 3e0099010..a6ab2ed8b 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -10,9 +10,25 @@
open Tacexpr
open Term
+open Names
open Proof_type
open Topconstr
+open Rawterm
val rawwit_orient : bool raw_abstract_argument_type
val wit_orient : bool closed_abstract_argument_type
val orient : bool Pcoq.Gram.Entry.e
+
+val rawwit_raw : constr_expr raw_abstract_argument_type
+val wit_raw : rawconstr closed_abstract_argument_type
+val raw : constr_expr Pcoq.Gram.Entry.e
+
+type 'id gen_place= ('id * hyp_location_flag,unit) location
+
+type loc_place = identifier Util.located gen_place
+type place = identifier gen_place
+
+val rawwit_hloc : loc_place raw_abstract_argument_type
+val wit_hloc : place closed_abstract_argument_type
+val hloc : loc_place Pcoq.Gram.Entry.e
+
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e55df2bf1..65bed9007 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -242,6 +242,14 @@ TACTIC EXTEND Evar
[ let_evar Names.Anonymous typ ]
END
+open Tacexpr
+
+TACTIC EXTEND Instantiate
+ [ "Instantiate" "(" integer(i) ":=" raw(c) ")" hloc(hl) ] ->
+ [ instantiate i c hl ]
+END
+
+
(** Nijmegen "step" tactic for setoid rewriting *)
open Tacticals
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2b2f39e1e..4a395fa31 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -663,12 +663,13 @@ 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,idh) ->
+(* | TacInstantiate (n,c,idh) ->
TacInstantiate (n,intern_constr ist c,
(match idh with
ConclLocation () -> ConclLocation ()
| HypLocation (id,hloc) ->
- HypLocation(intern_hyp_or_metaid ist id,hloc)))
+ HypLocation(intern_hyp_or_metaid ist id,hloc)))
+*)
(* Automation tactics *)
| TacTrivial l -> TacTrivial l
@@ -1717,13 +1718,13 @@ 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,idh) -> h_instantiate n (fst c)
+(* | TacInstantiate (n,c,idh) -> h_instantiate n (fst c)
(* pf_interp_constr ist gl c *)
(match idh with
ConclLocation () -> ConclLocation ()
| HypLocation (id,hloc) ->
HypLocation(interp_hyp ist gl id,hloc))
-
+*)
(* Automation tactics *)
| TacTrivial l -> Auto.h_trivial l
| TacAuto (n, l) -> Auto.h_auto n l
@@ -1976,8 +1977,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl)
| TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
| TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp)
- | TacInstantiate (n,c,ido) -> TacInstantiate (n,subst_rawconstr subst c,ido)
-
+(*| TacInstantiate (n,c,ido) -> TacInstantiate (n,subst_rawconstr subst c,ido)
+*)
(* Automation tactics *)
| TacTrivial l -> TacTrivial l
| TacAuto (n,l) -> TacAuto (n,l)
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 49af044c5..88cdf43c5 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -87,9 +87,18 @@ val interp_genarg :
val intern_genarg :
glob_sign -> raw_generic_argument -> glob_generic_argument
+val intern_constr :
+ glob_sign -> constr_expr -> rawconstr_and_expr
+
+val intern_hyp :
+ glob_sign -> identifier Util.located -> identifier Util.located
+
val subst_genarg :
Names.substitution -> glob_generic_argument -> glob_generic_argument
+val subst_rawconstr :
+ Names.substitution -> rawconstr_and_expr -> rawconstr_and_expr
+
(* Interprets any expression *)
val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value
@@ -101,6 +110,9 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr
val interp_tac_gen : (identifier * value) list ->
debug_info -> raw_tactic_expr -> tactic
+val interp_hyp : interp_sign -> goal sigma ->
+ identifier Util.located -> identifier
+
(* Initial call for interpretation *)
val glob_tactic : raw_tactic_expr -> glob_tactic_expr
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 23092a733..8855dda46 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -539,7 +539,7 @@ 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,ConclLocation ()) ->
+(* | TacInstantiate (n,c,ConclLocation ()) ->
hov 1 (str "instantiate" ++ spc() ++
hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
pr_lconstrarg env c ++ str ")" ))
@@ -548,7 +548,7 @@ and pr_atom1 env = function
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-03 06:32:05 +0000