diff options
31 files changed, 402 insertions, 345 deletions
@@ -142,7 +142,8 @@ parsing/ppconstr.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ kernel/environ.cmi parsing/coqast.cmi parsing/pptactic.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ proofs/tacexpr.cmo pretyping/rawterm.cmi proofs/proof_type.cmi \ - pretyping/pretyping.cmi lib/pp.cmi library/libnames.cmi interp/genarg.cmi + pretyping/pretyping.cmi interp/ppextend.cmi lib/pp.cmi \ + library/libnames.cmi interp/genarg.cmi parsing/prettyp.cmi: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ kernel/sign.cmi kernel/safe_typing.cmi pretyping/reductionops.cmi \ lib/pp.cmi library/nametab.cmi kernel/names.cmi library/libnames.cmi \ @@ -358,8 +359,8 @@ translate/ppconstrnew.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ library/libnames.cmi interp/genarg.cmi parsing/extend.cmi \ kernel/environ.cmi parsing/coqast.cmi translate/pptacticnew.cmi: interp/topconstr.cmi proofs/tacexpr.cmo \ - proofs/proof_type.cmi lib/pp.cmi kernel/names.cmi interp/genarg.cmi \ - kernel/environ.cmi + proofs/proof_type.cmi interp/ppextend.cmi lib/pp.cmi kernel/names.cmi \ + interp/genarg.cmi kernel/environ.cmi translate/ppvernacnew.cmi: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \ parsing/pptactic.cmi interp/ppextend.cmi parsing/ppconstr.cmi lib/pp.cmi \ @@ -1206,15 +1207,15 @@ parsing/ppconstr.cmx: lib/util.cmx kernel/univ.cmx interp/topconstr.cmx \ parsing/ppconstr.cmi parsing/pptactic.cmo: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ proofs/tacexpr.cmo pretyping/rawterm.cmi parsing/printer.cmi \ - translate/ppconstrnew.cmi parsing/ppconstr.cmi lib/pp.cmi \ - pretyping/pattern.cmi lib/options.cmi library/nametab.cmi \ + interp/ppextend.cmi translate/ppconstrnew.cmi parsing/ppconstr.cmi \ + lib/pp.cmi pretyping/pattern.cmi lib/options.cmi library/nametab.cmi \ kernel/names.cmi library/nameops.cmi library/libnames.cmi \ interp/genarg.cmi parsing/extend.cmi lib/dyn.cmi interp/constrextern.cmi \ kernel/closure.cmi parsing/pptactic.cmi parsing/pptactic.cmx: lib/util.cmx interp/topconstr.cmx kernel/term.cmx \ proofs/tacexpr.cmx pretyping/rawterm.cmx parsing/printer.cmx \ - translate/ppconstrnew.cmx parsing/ppconstr.cmx lib/pp.cmx \ - pretyping/pattern.cmx lib/options.cmx library/nametab.cmx \ + interp/ppextend.cmx translate/ppconstrnew.cmx parsing/ppconstr.cmx \ + lib/pp.cmx pretyping/pattern.cmx lib/options.cmx library/nametab.cmx \ kernel/names.cmx library/nameops.cmx library/libnames.cmx \ interp/genarg.cmx parsing/extend.cmx lib/dyn.cmx interp/constrextern.cmx \ kernel/closure.cmx parsing/pptactic.cmi @@ -1859,7 +1860,7 @@ tactics/eqdecide.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \ lib/pp.cmx parsing/pcoq.cmx pretyping/pattern.cmx lib/options.cmx \ kernel/names.cmx library/nameops.cmx pretyping/matching.cmx \ tactics/hipattern.cmx tactics/hiddentac.cmx library/global.cmx \ - interp/genarg.cmx tactics/extratactics.cmx tactics/equality.cmx \ + interp/genarg.cmx tactics/extratactics.cmi tactics/equality.cmx \ parsing/egrammar.cmx kernel/declarations.cmx interp/coqlib.cmx \ toplevel/cerrors.cmx tactics/auto.cmx tactics/equality.cmo: toplevel/vernacexpr.cmo lib/util.cmi kernel/univ.cmi \ @@ -1904,30 +1905,6 @@ tactics/extraargs.cmx: lib/util.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx library/nameops.cmx \ toplevel/metasyntax.cmx interp/genarg.cmx parsing/extend.cmx \ tactics/extraargs.cmi -tactics/extratactics.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ - kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ - tactics/tacinterp.cmi proofs/tacexpr.cmo library/summary.cmi \ - tactics/setoid_replace.cmi proofs/refiner.cmi tactics/refine.cmi \ - pretyping/rawterm.cmi parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi \ - lib/options.cmi kernel/names.cmi kernel/mod_subst.cmi \ - library/libobject.cmi library/libnames.cmi library/lib.cmi \ - tactics/leminv.cmi tactics/inv.cmi library/global.cmi interp/genarg.cmi \ - tactics/extraargs.cmi pretyping/evd.cmi tactics/evar_tactics.cmi \ - tactics/equality.cmi parsing/egrammar.cmi tactics/contradiction.cmi \ - interp/constrintern.cmi toplevel/cerrors.cmi tactics/autorewrite.cmi \ - tactics/extratactics.cmi -tactics/extratactics.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ - kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ - tactics/tacinterp.cmx proofs/tacexpr.cmx library/summary.cmx \ - tactics/setoid_replace.cmx proofs/refiner.cmx tactics/refine.cmx \ - pretyping/rawterm.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \ - lib/options.cmx kernel/names.cmx kernel/mod_subst.cmx \ - library/libobject.cmx library/libnames.cmx library/lib.cmx \ - tactics/leminv.cmx tactics/inv.cmx library/global.cmx interp/genarg.cmx \ - tactics/extraargs.cmx pretyping/evd.cmx tactics/evar_tactics.cmx \ - tactics/equality.cmx parsing/egrammar.cmx tactics/contradiction.cmx \ - interp/constrintern.cmx toplevel/cerrors.cmx tactics/autorewrite.cmx \ - tactics/extratactics.cmi tactics/hiddentac.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \ proofs/tacmach.cmi proofs/tacexpr.cmo proofs/refiner.cmi \ pretyping/rawterm.cmi proofs/proof_type.cmi interp/genarg.cmi \ @@ -2432,22 +2409,22 @@ translate/ppconstrnew.cmx: lib/util.cmx kernel/univ.cmx interp/topconstr.cmx \ parsing/ast.cmx translate/ppconstrnew.cmi translate/pptacticnew.cmo: lib/util.cmi interp/topconstr.cmi \ pretyping/termops.cmi kernel/term.cmi proofs/tactic_debug.cmi \ - proofs/tacexpr.cmo pretyping/rawterm.cmi parsing/printer.cmi \ - parsing/pptactic.cmi interp/ppextend.cmi translate/ppconstrnew.cmi \ - lib/pp.cmi lib/options.cmi library/nametab.cmi kernel/names.cmi \ - library/nameops.cmi library/libnames.cmi library/global.cmi \ - interp/genarg.cmi parsing/extend.cmi kernel/environ.cmi \ - parsing/egrammar.cmi lib/dyn.cmi interp/constrextern.cmi \ - kernel/closure.cmi translate/pptacticnew.cmi + proofs/tacexpr.cmo pretyping/rawterm.cmi proofs/proof_type.cmi \ + parsing/printer.cmi parsing/pptactic.cmi interp/ppextend.cmi \ + translate/ppconstrnew.cmi lib/pp.cmi lib/options.cmi library/nametab.cmi \ + kernel/names.cmi library/nameops.cmi library/libnames.cmi \ + library/global.cmi interp/genarg.cmi parsing/extend.cmi \ + kernel/environ.cmi parsing/egrammar.cmi lib/dyn.cmi \ + interp/constrextern.cmi kernel/closure.cmi translate/pptacticnew.cmi translate/pptacticnew.cmx: lib/util.cmx interp/topconstr.cmx \ pretyping/termops.cmx kernel/term.cmx proofs/tactic_debug.cmx \ - proofs/tacexpr.cmx pretyping/rawterm.cmx parsing/printer.cmx \ - parsing/pptactic.cmx interp/ppextend.cmx translate/ppconstrnew.cmx \ - lib/pp.cmx lib/options.cmx library/nametab.cmx kernel/names.cmx \ - library/nameops.cmx library/libnames.cmx library/global.cmx \ - interp/genarg.cmx parsing/extend.cmx kernel/environ.cmx \ - parsing/egrammar.cmx lib/dyn.cmx interp/constrextern.cmx \ - kernel/closure.cmx translate/pptacticnew.cmi + proofs/tacexpr.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ + parsing/printer.cmx parsing/pptactic.cmx interp/ppextend.cmx \ + translate/ppconstrnew.cmx lib/pp.cmx lib/options.cmx library/nametab.cmx \ + kernel/names.cmx library/nameops.cmx library/libnames.cmx \ + library/global.cmx interp/genarg.cmx parsing/extend.cmx \ + kernel/environ.cmx parsing/egrammar.cmx lib/dyn.cmx \ + interp/constrextern.cmx kernel/closure.cmx translate/pptacticnew.cmi translate/ppvernacnew.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tacinterp.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \ @@ -2607,7 +2584,7 @@ contrib/correctness/ptactic.cmx: toplevel/vernacentries.cmx lib/util.cmx \ parsing/printer.cmx pretyping/pretyping.cmx lib/pp.cmx proofs/pfedit.cmx \ pretyping/pattern.cmx lib/options.cmx library/nametab.cmx \ kernel/names.cmx library/nameops.cmx library/libnames.cmx \ - library/global.cmx tactics/extratactics.cmx pretyping/evd.cmx \ + library/global.cmx tactics/extratactics.cmi pretyping/evd.cmx \ tactics/equality.cmx library/decl_kinds.cmx interp/coqlib.cmx \ contrib/correctness/ptactic.cmi contrib/correctness/ptyping.cmo: lib/util.cmi pretyping/typing.cmi \ @@ -3063,14 +3040,14 @@ contrib/interface/dad.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ contrib/interface/debug_tac.cmo: lib/util.cmi tactics/tacticals.cmi \ proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ proofs/refiner.cmi proofs/proof_type.cmi proofs/proof_trees.cmi \ - parsing/printer.cmi parsing/pptactic.cmi lib/pp.cmi interp/genarg.cmi \ - parsing/coqast.cmi toplevel/cerrors.cmi parsing/ast.cmi \ + parsing/printer.cmi parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi \ + interp/genarg.cmi parsing/coqast.cmi toplevel/cerrors.cmi parsing/ast.cmi \ contrib/interface/debug_tac.cmi contrib/interface/debug_tac.cmx: lib/util.cmx tactics/tacticals.cmx \ proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ proofs/refiner.cmx proofs/proof_type.cmx proofs/proof_trees.cmx \ - parsing/printer.cmx parsing/pptactic.cmx lib/pp.cmx interp/genarg.cmx \ - parsing/coqast.cmx toplevel/cerrors.cmx parsing/ast.cmx \ + parsing/printer.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \ + interp/genarg.cmx parsing/coqast.cmx toplevel/cerrors.cmx parsing/ast.cmx \ contrib/interface/debug_tac.cmi contrib/interface/history.cmo: contrib/interface/paths.cmi \ contrib/interface/history.cmi @@ -3188,20 +3165,20 @@ contrib/interface/vtp.cmx: contrib/interface/ascent.cmi \ contrib/interface/vtp.cmi contrib/interface/xlate.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi kernel/term.cmi proofs/tacexpr.cmo \ - pretyping/rawterm.cmi parsing/ppconstr.cmi lib/options.cmi \ - kernel/names.cmi library/libnames.cmi library/goptions.cmi \ - interp/genarg.cmi contrib/field/field.cmo tactics/extraargs.cmi \ - parsing/extend.cmi tactics/eauto.cmi library/decl_kinds.cmo \ - lib/bigint.cmi parsing/ast.cmi contrib/interface/ascent.cmi \ - contrib/interface/xlate.cmi + pretyping/rawterm.cmi parsing/ppconstr.cmi parsing/pcoq.cmi \ + lib/options.cmi kernel/names.cmi library/libnames.cmi \ + library/goptions.cmi interp/genarg.cmi contrib/field/field.cmo \ + tactics/extraargs.cmi parsing/extend.cmi tactics/eauto.cmi \ + library/decl_kinds.cmo lib/bigint.cmi parsing/ast.cmi \ + contrib/interface/ascent.cmi contrib/interface/xlate.cmi contrib/interface/xlate.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ interp/topconstr.cmx kernel/term.cmx proofs/tacexpr.cmx \ - pretyping/rawterm.cmx parsing/ppconstr.cmx lib/options.cmx \ - kernel/names.cmx library/libnames.cmx library/goptions.cmx \ - interp/genarg.cmx contrib/field/field.cmx tactics/extraargs.cmx \ - parsing/extend.cmx tactics/eauto.cmx library/decl_kinds.cmx \ - lib/bigint.cmx parsing/ast.cmx contrib/interface/ascent.cmi \ - contrib/interface/xlate.cmi + pretyping/rawterm.cmx parsing/ppconstr.cmx parsing/pcoq.cmx \ + lib/options.cmx kernel/names.cmx library/libnames.cmx \ + library/goptions.cmx interp/genarg.cmx contrib/field/field.cmx \ + tactics/extraargs.cmx parsing/extend.cmx tactics/eauto.cmx \ + library/decl_kinds.cmx lib/bigint.cmx parsing/ast.cmx \ + contrib/interface/ascent.cmi contrib/interface/xlate.cmi contrib/jprover/jall.cmo: lib/pp.cmi contrib/jprover/opname.cmi \ contrib/jprover/jtunify.cmi contrib/jprover/jterm.cmi \ contrib/jprover/jlogic.cmi contrib/jprover/jall.cmi @@ -3593,72 +3570,66 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/misc.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/mlvalues.h \ + /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ kernel/byterun/coq_jumptbl.h coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h + kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/memory.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /home/logical/local/lib/ocaml/caml/alloc.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/fail.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/lib/ocaml/caml/alloc.h coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/misc.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/mlvalues.h \ + /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ kernel/byterun/coq_jumptbl.h coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h + kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/memory.h coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /home/logical/local/lib/ocaml/caml/alloc.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/fail.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/lib/ocaml/caml/alloc.h @@ -30,7 +30,7 @@ Tactics - Omega now handles arbitrary precision integers - Idtac can now be left implicit in a [...|...] construct: for instance, [ foo | | bar ] stands for [ foo | idtac | bar ]. (doc TODO). - +- "Tactic Notation" extended to allow notations of tacticals (doc TODO). Modules @@ -1511,6 +1511,14 @@ proofs/tacexpr.cmx: proofs/tacexpr.ml $(SHOW)'OCAMLOPT -rectypes $<' $(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $< +translate/pptacticnew.cmo: translate/pptacticnew.ml + $(SHOW)'OCAMLC -rectypes $<' + $(HIDE)$(OCAMLC) -rectypes $(BYTEFLAGS) -c $< + +translate/pptacticnew.cmx: translate/pptacticnew.ml + $(SHOW)'OCAMLOPT -rectypes $<' + $(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $< + ML4FILES += lib/pp.ml4 lib/compat.ml4 lib/compat.cmo: lib/compat.ml4 diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4 index 939c67917..b02b06e86 100644 --- a/contrib/interface/debug_tac.ml4 +++ b/contrib/interface/debug_tac.ml4 @@ -263,9 +263,14 @@ and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tacti by the list of integers given as extra arguments. *) +let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level +let globwit_main_tactic = globwit_tactic Pcoq.Tactic.tactic_main_level +let wit_main_tactic = wit_tactic Pcoq.Tactic.tactic_main_level + + let on_then = function [t1;t2;l] -> - let t1 = out_gen wit_tactic t1 in - let t2 = out_gen wit_tactic t2 in + let t1 = out_gen wit_main_tactic t1 in + let t2 = out_gen wit_main_tactic t2 in let l = out_gen (wit_list0 wit_int) l in tclTHEN_i (Tacinterp.eval_tactic t1) (fun i -> @@ -276,8 +281,8 @@ let on_then = function [t1;t2;l] -> | _ -> anomaly "bad arguments for on_then";; let mkOnThen t1 t2 selected_indices = - let a = in_gen rawwit_tactic t1 in - let b = in_gen rawwit_tactic t2 in + let a = in_gen rawwit_main_tactic t1 in + let b = in_gen rawwit_main_tactic t2 in let l = in_gen (wit_list0 rawwit_int) selected_indices in TacAtom (dummy_loc, TacExtend (dummy_loc, "OnThen", [a;b;l]));; @@ -364,8 +369,8 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) = | Report_node(false, n, rl) -> let selected_indices = select_success 1 rl in TacAtom (dummy_loc,TacExtend (dummy_loc,"OnThen", - [in_gen globwit_tactic a; - in_gen globwit_tactic b; + [in_gen globwit_main_tactic a; + in_gen globwit_main_tactic b; in_gen (wit_list0 globwit_int) selected_indices])) | Failed n -> TacId "" | Tree_fail r -> reconstruct_success_tac a r diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index b500d7d22..8db615add 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -683,6 +683,8 @@ let xlate_intro_patt_opt = function None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp) +let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level + let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) = function | TacVoid -> @@ -869,7 +871,10 @@ and xlate_tactic = and xlate_tac = function | TacExtend (_, "firstorder", tac_opt::l) -> - let t1 = match out_gen (wit_opt rawwit_tactic) tac_opt with + let t1 = + match + out_gen (wit_opt rawwit_main_tactic) tac_opt + with | None -> CT_coerce_NONE_to_TACTIC_OPT CT_none | Some t2 -> CT_coerce_TACTIC_COM_to_TACTIC_OPT (xlate_tactic t2) in (match l with @@ -983,14 +988,14 @@ and xlate_tac = if b then CT_rewrite_lr (c, bindl, id) else CT_rewrite_rl (c, bindl, id) | TacExtend (_,"conditionalrewrite", [t; b; cbindl]) -> - let t = out_gen rawwit_tactic t in + let t = out_gen rawwit_main_tactic t in let b = out_gen Extraargs.rawwit_orient b in let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in let c = xlate_formula c and bindl = xlate_bindings bindl in if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE) else CT_condrewrite_rl (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE) | TacExtend (_,"conditionalrewrite", [t; b; cbindl; id]) -> - let t = out_gen rawwit_tactic t in + let t = out_gen rawwit_main_tactic t in let b = out_gen Extraargs.rawwit_orient b in let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in let c = xlate_formula c and bindl = xlate_bindings bindl in @@ -1055,7 +1060,7 @@ and xlate_tac = match t with [t0] -> CT_coerce_TACTIC_COM_to_TACTIC_OPT - (xlate_tactic(out_gen rawwit_tactic t0)) + (xlate_tactic(out_gen rawwit_main_tactic t0)) | [] -> CT_coerce_NONE_to_TACTIC_OPT CT_none | _ -> assert false in CT_autorewrite (CT_id_ne_list(fst, id_list1), t1) @@ -1241,8 +1246,8 @@ and coerce_genarg_to_TARG x = (CT_coerce_FORMULA_to_SCOMMENT_CONTENT (xlate_formula (out_gen rawwit_constr x))) | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument" | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument" - | TacticArgType -> - let t = xlate_tactic (out_gen rawwit_tactic x) in + | TacticArgType n -> + let t = xlate_tactic (out_gen (rawwit_tactic n) x) in CT_coerce_TACTIC_COM_to_TARG t | OpenConstrArgType b -> CT_coerce_SCOMMENT_CONTENT_to_TARG @@ -1335,8 +1340,8 @@ let coerce_genarg_to_VARG x = (CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula (out_gen rawwit_constr x))) | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument" | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument" - | TacticArgType -> - let t = xlate_tactic (out_gen rawwit_tactic x) in + | TacticArgType n -> + let t = xlate_tactic (out_gen (rawwit_tactic n) x) in CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t) | OpenConstrArgType _ -> xlate_error "TODO: generic open constr" | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings" @@ -1653,7 +1658,7 @@ let rec xlate_vernac = let formula_list = out_gen (wit_list1 rawwit_constr) (List.nth largs 1) in let t = if List.length largs = 4 then - out_gen rawwit_tactic (List.nth largs (if in_v8 then 2 else 3)) + out_gen rawwit_main_tactic (List.nth largs (if in_v8 then 2 else 3)) else TacId "" in let base = diff --git a/interp/genarg.ml b/interp/genarg.ml index 2b01a2034..f81425eb8 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -33,7 +33,7 @@ type argument_type = | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | TacticArgType + | TacticArgType of int | OpenConstrArgType of bool | ConstrWithBindingsArgType | BindingsArgType @@ -140,9 +140,9 @@ let rawwit_constr_may_eval = ConstrMayEvalArgType let globwit_constr_may_eval = ConstrMayEvalArgType let wit_constr_may_eval = ConstrMayEvalArgType -let rawwit_tactic = TacticArgType -let globwit_tactic = TacticArgType -let wit_tactic = TacticArgType +let rawwit_tactic n = TacticArgType n +let globwit_tactic n = TacticArgType n +let wit_tactic n = TacticArgType n let rawwit_open_constr_gen b = OpenConstrArgType b let globwit_open_constr_gen b = OpenConstrArgType b diff --git a/interp/genarg.mli b/interp/genarg.mli index 042520151..9609576a4 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -161,9 +161,9 @@ val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type (* TODO: transformer tactic en extra arg *) -val rawwit_tactic : ('ta,constr_expr,'ta) abstract_argument_type -val globwit_tactic : ('ta,rawconstr_and_expr,'ta) abstract_argument_type -val wit_tactic : ('ta,constr,'ta) abstract_argument_type +val rawwit_tactic : int -> ('ta,constr_expr,'ta) abstract_argument_type +val globwit_tactic : int -> ('ta,rawconstr_and_expr,'ta) abstract_argument_type +val wit_tactic : int -> ('ta,constr,'ta) abstract_argument_type val wit_list0 : ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type @@ -238,7 +238,7 @@ type argument_type = | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | TacticArgType + | TacticArgType of int | OpenConstrArgType of bool | ConstrWithBindingsArgType | BindingsArgType diff --git a/lib/compat.ml4 b/lib/compat.ml4 index 0947f5fb8..7ea3ff669 100644 --- a/lib/compat.ml4 +++ b/lib/compat.ml4 @@ -20,7 +20,9 @@ let unloc (b,e) = let loc = (b.Lexing.pos_cnum,e.Lexing.pos_cnum) in (* Ensure that we unpack a char location that was encoded as a line-col location by make_loc *) +(* Gram.Entry.parse may send bad loc in 3.08, see caml-bugs #2954 assert (dummy_loc = (b,e) or make_loc loc = (b,e)); +*) loc end else diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 061efa49e..c0207f077 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -31,7 +31,7 @@ let rec make_rawwit loc = function | ConstrArgType -> <:expr< Genarg.rawwit_constr >> | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >> | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> - | TacticArgType -> <:expr< Genarg.rawwit_tactic >> + | TacticArgType n -> <:expr< Genarg.rawwit_tactic $mlexpr_of_int n$ >> | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >> | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> @@ -57,7 +57,7 @@ let rec make_globwit loc = function | SortArgType -> <:expr< Genarg.globwit_sort >> | ConstrArgType -> <:expr< Genarg.globwit_constr >> | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> - | TacticArgType -> <:expr< Genarg.globwit_tactic >> + | TacticArgType n -> <:expr< Genarg.globwit_tactic $mlexpr_of_int n$ >> | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> | OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >> | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> @@ -83,7 +83,7 @@ let rec make_wit loc = function | SortArgType -> <:expr< Genarg.wit_sort >> | ConstrArgType -> <:expr< Genarg.wit_constr >> | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> - | TacticArgType -> <:expr< Genarg.wit_tactic >> + | TacticArgType n -> <:expr< Genarg.wit_tactic $mlexpr_of_int n$ >> | RedExprArgType -> <:expr< Genarg.wit_red_expr >> | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >> | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index cee0a1ea9..54e069512 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -27,8 +27,9 @@ type all_grammar_command = | Notation of (precedence * tolerability list) * notation_grammar | Grammar of grammar_command | TacticGrammar of - (string * (string * grammar_production list) * - (Names.dir_path * Tacexpr.glob_tactic_expr)) + int * + (string * grammar_production list * + (Names.dir_path * Tacexpr.glob_tactic_expr)) list val extend_grammar : all_grammar_command -> unit @@ -39,21 +40,18 @@ type grammar_tactic_production = | TacNonTerm of loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option val extend_tactic_grammar : - string -> (string * grammar_tactic_production list) list -> unit + string -> grammar_tactic_production list list -> unit val extend_vernac_command_grammar : - string -> (string * grammar_tactic_production list) list -> unit + string -> grammar_tactic_production list list -> unit val get_extend_tactic_grammars : - unit -> (string * (string * grammar_tactic_production list) list) list + unit -> (string * grammar_tactic_production list list) list val get_extend_vernac_grammars : - unit -> (string * (string * grammar_tactic_production list) list) list + unit -> (string * grammar_tactic_production list list) list val reset_extend_grammars_v8 : unit -> unit -val subst_all_grammar_command : - substitution -> all_grammar_command -> all_grammar_command - -val interp_entry_name : string -> string -> +val interp_entry_name : int -> string -> string -> entry_type * Token.t Gramext.g_symbol val recover_notation_grammar : diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 648bb2829..097f38f01 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -246,17 +246,25 @@ GEXTEND Gram GLOBAL: syntax; univ: - [ [ univ = IDENT -> + [ [ univ = IDENT -> set_default_action_parser (parser_type_from_name univ); univ ] ] ; + grammar_tactic_level: + [ [ IDENT "simple_tactic" -> 0 + | IDENT "tactic1" -> 1 + | IDENT "tactic2" -> 2 + | IDENT "tactic3" -> 3 + | IDENT "tactic4" -> 4 + | IDENT "tactic5" -> 5 ] ] + ; syntax: [ [ IDENT "Token"; s = lstring -> Pp.warning "Token declarations are now useless"; VernacNop - | IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic"; + | IDENT "Grammar"; IDENT "tactic"; lev = grammar_tactic_level; OPT [ ":"; IDENT "tactic" ]; ":="; OPT "|"; tl = LIST0 grammar_tactic_rule SEP "|" -> - VernacTacticGrammar tl + VernacTacticGrammar (lev,tl) | IDENT "Grammar"; u = univ; tl = LIST1 grammar_entry SEP "with" -> @@ -416,8 +424,8 @@ GEXTEND Gram | -> None ]] ; grammar_tactic_rule: - [[ name = rule_name; "["; s = lstring; pil = LIST0 production_item; "]"; - "->"; "["; t = Tactic.tactic; "]" -> (name, (s,pil), t) ]] + [[ name = rule_name; "["; pil = LIST0 production_item; "]"; + "->"; "["; t = Tactic.tactic; "]" -> (name, pil, t) ]] ; grammar_rule: [[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->"; diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 8defe13c1..e73682d22 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -41,10 +41,11 @@ let arg_of_expr = function if !Options.v7 then GEXTEND Gram - GLOBAL: tactic Vernac_.command tactic_arg; + GLOBAL: tactic Vernac_.command tactic_arg + tactic_expr5 tactic_expr4 tactic_expr3 tactic_expr2; (* - GLOBAL: tactic_atom tactic_atom0 tactic_expr input_fun; + GLOBAL: tactic_atom tactic_atom0 input_fun; *) input_fun: [ [ l = base_ident -> Some l diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index 265675df8..9e0a10931 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -39,8 +39,6 @@ let arg_of_expr = function (* Tactics grammar rules *) -let tactic_expr = Gram.Entry.create "tactic:tactic_expr" - if not !Options.v7 then GEXTEND Gram GLOBAL: tactic Vernac_.command tactic_expr tactic_arg; diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index f0350946f..c21feb09e 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -693,9 +693,9 @@ GEXTEND Gram sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacNotation (local,c,Some(s,modl),None,sc) - | IDENT "Tactic"; IDENT "Notation"; s = ne_string; - pil = LIST0 production_item; ":="; t = Tactic.tactic -> - VernacTacticGrammar ["",(s,pil),t] + | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; + pil = LIST0 production_item; ":="; t = Tactic.tactic + -> VernacTacticGrammar (n,["",pil,t]) | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] @@ -705,6 +705,9 @@ GEXTEND Gram to factorize with other "Print"-based vernac entries *) ] ] ; + tactic_level: + [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ] + ; locality: [ [ IDENT "Local" -> true | -> false ] ] ; diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index cc7bb3dad..135a9f8d1 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -52,7 +52,7 @@ let grammar_delete e rls = List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev)) (List.rev rls) -(* grammar_object is the superclass of all grammar entry *) +(* grammar_object is the superclass of all grammar entries *) module type Gramobj = sig type grammar_object @@ -390,10 +390,20 @@ module Tactic = (* Main entries for ltac *) let tactic_arg = Gram.Entry.create "tactic:tactic_arg" - let tactic = make_gen_entry utactic rawwit_tactic "tactic" + (* For v8: *) + let tactic_expr = Gram.Entry.create "tactic:tactic_expr" + (* For v7: *) + let tactic_expr2 = Gram.Entry.create "tactic:tactic_expr2" + let tactic_expr3 = Gram.Entry.create "tactic:tactic_expr3" + let tactic_expr4 = Gram.Entry.create "tactic:tactic_expr4" + let tactic_expr5 = Gram.Entry.create "tactic:tactic_expr5" + + let tactic_main_level = 5 + let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic" (* Main entry for quotations *) let tactic_eoi = eoi_entry tactic + end diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 2fdb91254..c073a3d9f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -25,7 +25,10 @@ val lexer : Token.lexer module Gram : Grammar.S with type te = Token.t +(* The superclass of all grammar entries *) type grammar_object + +(* The type of typed grammar objects *) type typed_entry val type_of_typed_entry : typed_entry -> Extend.entry_type @@ -39,7 +42,7 @@ val symbol_of_production : Gramext.g_assoc option -> constr_entry -> bool -> constr_production_entry -> Token.t Gramext.g_symbol val grammar_extend : - 'a Gram.Entry.e -> Gramext.position option -> + grammar_object Gram.Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * (Token.t Gramext.g_symbol list * Gramext.g_action) list) list -> unit @@ -168,8 +171,16 @@ module Tactic : val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e val tactic_arg : raw_tactic_arg Gram.Entry.e + val tactic_expr : raw_tactic_expr Gram.Entry.e + val tactic_main_level : int val tactic : raw_tactic_expr Gram.Entry.e val tactic_eoi : raw_tactic_expr Gram.Entry.e + + (* For v7 *) + val tactic_expr2 : raw_tactic_expr Gram.Entry.e + val tactic_expr3 : raw_tactic_expr Gram.Entry.e + val tactic_expr4 : raw_tactic_expr Gram.Entry.e + val tactic_expr5 : raw_tactic_expr Gram.Entry.e end module Vernac_ : diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 8e409a086..0dc646198 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -19,6 +19,7 @@ open Topconstr open Genarg open Libnames open Pattern +open Ppextend let pr_red_expr = Ppconstr.pr_red_expr let pr_may_eval = Ppconstr.pr_may_eval @@ -42,13 +43,16 @@ let declare_extra_tactic_pprule for_v8 s (tags,prods) = if for_v8 then Hashtbl.add prtac_tab (s,tags) prods type 'a raw_extra_genarg_printer = - (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> + (tolerability -> raw_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds type 'a glob_extra_genarg_printer = - (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + (rawconstr_and_expr -> std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds type 'a extra_genarg_printer = - (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds let genarg_pprule_v7 = ref Stringmap.empty @@ -271,7 +275,7 @@ let rec pr_raw_generic prc prlc prtac prref x = | RedExprArgType -> pr_arg (pr_red_expr (prc,prref)) (out_gen rawwit_red_expr x) - | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x) + | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (rawwit_tactic n) x) | OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x) @@ -318,7 +322,7 @@ let rec pr_glob_generic prc prlc prtac x = | RedExprArgType -> pr_arg (pr_red_expr (prc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x) - | TacticArgType -> pr_arg prtac (out_gen globwit_tactic x) + | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (globwit_tactic n) x) | OpenConstrArgType b -> pr_arg prc (snd (out_gen (globwit_open_constr_gen b) x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x) @@ -364,7 +368,7 @@ let rec pr_generic prc prlc prtac x = pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x) | RedExprArgType -> pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x) - | TacticArgType -> pr_arg prtac (out_gen wit_tactic x) + | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (wit_tactic n) x) | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x) @@ -394,7 +398,9 @@ let rec pr_tacarg_using_rule pr_gen = function | [], [] -> mt () | _ -> failwith "Inconsistent arguments of extended tactic" -let pr_extend_gen prgen s l = +let surround p = hov 1 (str"(" ++ p ++ str")") + +let pr_extend_gen prgen lev s l = let tab = if Options.do_translate() or not !Options.v7 then prtac_tab else prtac_tab_v7 @@ -407,12 +413,13 @@ let pr_extend_gen prgen s l = if Options.do_translate() & n > 2 & String.sub s (n-2) 2 = "v7" then String.sub s 0 (n-2) ^ "v8" else s in - let (s,pl) = Hashtbl.find tab (s,tags) in - str s ++ pr_tacarg_using_rule prgen (pl,l) + let (lev',pl) = Hashtbl.find tab (s,tags) in + let p = pr_tacarg_using_rule prgen (pl,l) in + if lev' > lev then surround p else p with Not_found -> str s ++ prlist prgen l ++ str " (* Generic printer *)" -let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) = +let make_pr_tac (pr_tac_level,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) = let pr_bindings = pr_bindings pr_constr pr_constr in let pr_bindings_no_with = pr_bindings_no_with pr_constr pr_constr in @@ -436,9 +443,9 @@ let rec pr_atom0 = function (* Main tactic printer *) and pr_atom1 = function - | TacExtend (_,s,l) -> pr_extend pr_constr pr_constr pr_tac s l + | TacExtend (_,s,l) -> pr_extend pr_constr pr_constr pr_tac_level 1 s l | TacAlias (_,s,l,_) -> - pr_extend pr_constr pr_constr pr_tac s (List.map snd l) + pr_extend pr_constr pr_constr pr_tac_level 1 s (List.map snd l) (* Basic tactics *) | TacIntroPattern [] as t -> pr_atom0 t @@ -569,7 +576,7 @@ and pr_atom1 = function | TacRight l -> hov 1 (str "Right" ++ pr_bindings l) | TacSplit (_,l) -> hov 1 (str "Split" ++ pr_bindings l) | TacAnyConstructor (Some t) -> - hov 1 (str "Constructor" ++ pr_arg pr_tac0 t) + hov 1 (str "Constructor" ++ pr_arg (pr_tac_level (0,E)) t) | TacAnyConstructor None as t -> pr_atom0 t | TacConstructor (n,l) -> hov 1 (str "Constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings l) @@ -628,6 +635,8 @@ and pr1 = function and pr2 = function | TacOrelse (t1,t2) -> hov 1 (pr1 t1 ++ str " Orelse" ++ brk (1,1) ++ pr3 t2) + | TacAtom (_,TacAlias (_,s,l,_)) -> + pr_extend pr_constr pr_constr pr_tac_level 2 s (List.map snd l) | t -> pr1 t (* Non closed prefix tactic expressions *) @@ -637,9 +646,13 @@ and pr3 = function | TacRepeat t -> hov 1 (str "Repeat" ++ spc () ++ pr3 t) | TacProgress t -> hov 1 (str "Progress" ++ spc () ++ pr3 t) | TacInfo t -> hov 1 (str "Info" ++ spc () ++ pr3 t) + | TacAtom (_,TacAlias (_,s,l,_)) -> + pr_extend pr_constr pr_constr pr_tac_level 3 s (List.map snd l) | t -> pr2 t and pr4 = function + | TacAtom (_,TacAlias (_,s,l,_)) -> + pr_extend pr_constr pr_constr pr_tac_level 4 s (List.map snd l) | t -> pr3 t (* THEN and THENS tactic expressions (printed as if parsed @@ -649,6 +662,8 @@ and pr5 = function hov 1 (pr5 t ++ str ";" ++ spc () ++ pr_tactic_seq_body tl) | TacThen (t1,t2) -> hov 1 (pr5 t1 ++ str ";" ++ spc () ++ pr4 t2) + | TacAtom (_,TacAlias (_,s,l,_)) -> + pr_extend pr_constr pr_constr pr_tac_level 5 s (List.map snd l) | t -> pr4 t (* Ltac tactic expressions *) @@ -714,14 +729,26 @@ and pr_tacarg0 = function and pr_tacarg1 = function | TacCall (_,f,l) -> hov 0 (pr_ref f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l) - | Tacexp t -> pr_tac t + | Tacexp t -> pr_tac_level (6,E) t | t -> pr_tacarg0 t and pr_tacarg x = pr_tacarg1 x and prtac x = pr6 x -in (prtac,pr0,pr_match_rule false pr_pat pr_tac) +and prtac_level (n,p) = + let n = match p with E -> n | L -> n-1 | Prec n -> n | Any -> 6 in + match n with + | 0 -> pr0 + | 1 -> pr1 + | 2 -> pr2 + | 3 -> pr3 + | 4 -> pr4 + | 5 -> pr5 + | 6 -> pr6 + | _ -> anomaly "Unknown tactic level" + +in (prtac_level,pr_match_rule false pr_pat (pr_tac_level (6,E))) let pr_raw_extend prc prlc prtac = pr_extend_gen (pr_raw_generic prc prlc prtac Ppconstrnew.pr_reference) @@ -733,8 +760,7 @@ let pr_extend prc prlc prtac = let pr_and_constr_expr pr (c,_) = pr c let rec glob_printers = - (pr_glob_tactic, - pr_glob_tactic0, + (pr_glob_tactic_level, pr_and_constr_expr Printer.pr_rawterm, Printer.pr_pattern, pr_or_var (pr_and_short_name pr_evaluable_reference), @@ -743,16 +769,15 @@ let rec glob_printers = pr_located pr_id, pr_glob_extend) -and pr_glob_tactic (t:glob_tactic_expr) = pi1 (make_pr_tac glob_printers) t +and pr_glob_tactic_level n (t:glob_tactic_expr) = + fst (make_pr_tac glob_printers) n t -and pr_glob_tactic0 t = pi2 (make_pr_tac glob_printers) t +and pr_glob_match_context t = + snd (make_pr_tac glob_printers) t -and pr_glob_match_context t = pi3 (make_pr_tac glob_printers) t - -let (pr_tactic,_,_) = +let (pr_tactic_level,_) = make_pr_tac - (pr_glob_tactic, - pr_glob_tactic0, + (pr_glob_tactic_level, Printer.prterm, Printer.pr_pattern, pr_evaluable_reference, @@ -760,3 +785,6 @@ let (pr_tactic,_,_) = pr_ltac_constant, pr_id, pr_extend) + +let pr_glob_tactic = pr_glob_tactic_level (6,E) +let pr_tactic = pr_tactic_level (6,E) diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 532664274..3738c57bb 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -15,6 +15,7 @@ open Pretyping open Proof_type open Topconstr open Rawterm +open Ppextend val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds @@ -22,15 +23,15 @@ val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds val pr_located : ('a -> std_ppcmds) -> 'a Util.located -> std_ppcmds type 'a raw_extra_genarg_printer = - (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds type 'a glob_extra_genarg_printer = - (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + (rawconstr_and_expr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds type 'a extra_genarg_printer = - (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds (* if the boolean is false then the extension applies only to old syntax *) @@ -44,7 +45,7 @@ type grammar_terminals = string option list (* if the boolean is false then the extension applies only to old syntax *) val declare_extra_tactic_pprule : bool -> string -> - argument_type list * (string * grammar_terminals) -> unit + argument_type list * (int * grammar_terminals) -> unit val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds @@ -58,27 +59,28 @@ val pr_tactic : Proof_type.tactic_expr -> std_ppcmds val pr_glob_generic: (rawconstr_and_expr -> std_ppcmds) -> (rawconstr_and_expr -> std_ppcmds) -> - (glob_tactic_expr -> std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> glob_generic_argument -> std_ppcmds val pr_raw_generic : (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> - (raw_tactic_expr -> std_ppcmds) -> + (tolerability -> raw_tactic_expr -> std_ppcmds) -> (Libnames.reference -> std_ppcmds) -> (constr_expr, raw_tactic_expr) generic_argument -> std_ppcmds val pr_raw_extend: (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> - (raw_tactic_expr -> std_ppcmds) -> string -> - raw_generic_argument list -> std_ppcmds + (tolerability -> raw_tactic_expr -> std_ppcmds) -> int -> + string -> raw_generic_argument list -> std_ppcmds val pr_glob_extend: (rawconstr_and_expr -> std_ppcmds) -> (rawconstr_and_expr -> std_ppcmds) -> - (glob_tactic_expr -> std_ppcmds) -> string -> - glob_generic_argument list -> std_ppcmds + (tolerability -> glob_tactic_expr -> std_ppcmds) -> int -> + string -> glob_generic_argument list -> std_ppcmds val pr_extend : (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> - (glob_tactic_expr -> std_ppcmds) -> string -> closed_generic_argument list -> std_ppcmds + (tolerability -> glob_tactic_expr -> std_ppcmds) -> int -> + string -> closed_generic_argument list -> std_ppcmds diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index d963d9450..9a5e43feb 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -275,7 +275,7 @@ let rec mlexpr_of_argtype loc = function | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> - | Genarg.TacticArgType -> <:expr< Genarg.TacticArgType >> + | Genarg.TacticArgType n -> <:expr< Genarg.TacticArgType $mlexpr_of_int n$ >> | Genarg.SortArgType -> <:expr< Genarg.SortArgType >> | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >> | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >> diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index dac09e8a8..3a20aad1b 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -36,6 +36,8 @@ let rec make_when loc = function <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >> | _::l -> make_when loc l +let is_tactic_arg = function TacticArgType _ -> true | _ -> false + let rec make_let e = function | [] -> e | TacNonTerm(loc,t,_,Some p)::l -> @@ -45,13 +47,13 @@ let rec make_let e = function let v = (* Special case for tactics which must be stored in algebraic form to avoid marshalling closures and to be reprinted *) - if t = TacticArgType then + if is_tactic_arg t then <:expr< ($v$, Tacinterp.eval_tactic $v$) >> else v in <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let e l -let add_clause s (_,pt,e) l = +let add_clause s (pt,e) l = let p = make_patt pt in let w = Some (make_when (MLast.loc_of_expr e) pt) in (p, w, make_let e pt)::l @@ -62,7 +64,7 @@ let rec extract_signature = function | _::l -> extract_signature l let check_unicity s l = - let l' = List.map (fun (_,l,_) -> extract_signature l) l in + let l' = List.map (fun (l,_) -> extract_signature l) l in if not (Util.list_distinct l') then Pp.warning_with Pp_control.err_ft ("Two distinct rules of tactic entry "^s^" have the same\n"^ @@ -82,7 +84,7 @@ let rec make_args = function let rec make_eval_tactic e = function | [] -> e - | TacNonTerm(loc,TacticArgType,_,Some p)::l -> + | TacNonTerm(loc,TacticArgType _,_,Some p)::l -> let loc = join_loc loc (MLast.loc_of_expr e) in let e = make_eval_tactic e l in (* Special case for tactics which must be stored in algebraic @@ -106,11 +108,8 @@ let mlexpr_terminals_of_grammar_production = function | TacTerm s -> <:expr< Some $mlexpr_of_string s$ >> | TacNonTerm (loc,nt,g,sopt) -> <:expr< None >> -let mlexpr_of_semi_clause = - mlexpr_of_pair mlexpr_of_string (mlexpr_of_list mlexpr_of_grammar_production) - let mlexpr_of_clause = - mlexpr_of_list (fun (a,b,c) -> mlexpr_of_semi_clause (a,b)) + mlexpr_of_list (fun (a,b) -> mlexpr_of_list mlexpr_of_grammar_production a) let rec make_tags loc = function | [] -> <:expr< [] >> @@ -121,19 +120,20 @@ let rec make_tags loc = function <:expr< [ $t$ :: $l$ ] >> | _::l -> make_tags loc l -let make_one_printing_rule (s,pt,e) = +let make_one_printing_rule (pt,e) = + let level = mlexpr_of_int 0 in (* only level 0 supported here *) let loc = MLast.loc_of_expr e in let prods = mlexpr_of_list mlexpr_terminals_of_grammar_production pt in - <:expr< ($make_tags loc pt$, ($str:s$, $prods$)) >> + <:expr< ($make_tags loc pt$, ($level$, $prods$)) >> let make_printing_rule = mlexpr_of_list make_one_printing_rule let new_tac_ext (s,cl) = (String.lowercase s, List.map - (fun (s,l,e) -> - (String.lowercase s, List.map - (function TacTerm s -> TacTerm (String.lowercase s) - | t -> t) l, + (fun (l,e) -> + (List.map (function + | TacTerm s -> TacTerm (String.lowercase s) + | t -> t) l, e)) cl) @@ -167,11 +167,13 @@ let rec contains_epsilon = function | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2 | ExtraArgType("hintbases") -> true | _ -> false -let is_atomic = - List.for_all - (function - TacTerm _ -> false - | TacNonTerm(_,t,_,_) -> contains_epsilon t) +let is_atomic = function + | TacTerm s :: l when + List.for_all (function + TacTerm _ -> false + | TacNonTerm(_,t,_,_) -> contains_epsilon t) l + -> [s] + | _ -> [] let declare_tactic loc s cl = let (s',cl') = new_tac_ext (s,cl) in @@ -180,7 +182,7 @@ let declare_tactic loc s cl = let se' = mlexpr_of_string s' in let pp = make_printing_rule cl in let gl = mlexpr_of_clause cl in - let hide_tac (_,p,e) = + let hide_tac (p,e) = (* reste a definir les fonctions cachees avec des noms frais *) let stac = "h_"^s' in let e = @@ -194,8 +196,8 @@ let declare_tactic loc s cl = let hidden = if List.length cl = 1 then List.map hide_tac cl' else [] in let se = mlexpr_of_string s in let atomic_tactics = - mlexpr_of_list (fun (s,_,_) -> mlexpr_of_string s) - (List.filter (fun (_,al,_) -> is_atomic al) cl') in + mlexpr_of_list mlexpr_of_string + (List.flatten (List.map (fun (al,_) -> is_atomic al) cl')) in <:str_item< declare open Pcoq; @@ -265,10 +267,8 @@ EXTEND declare_tactic_v7 loc s l ] ] ; tacrule: - [ [ "["; s = STRING; l = LIST0 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" - -> - if s = "" then Util.user_err_loc (loc,"",Pp.str "Tactic name is empty"); - (s,l,e) + [ [ "["; l = LIST0 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" + -> (l,e) ] ] ; tacargs: @@ -276,6 +276,7 @@ EXTEND let t, g = interp_entry_name loc e in TacNonTerm (loc, t, g, Some s) | s = STRING -> + if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal"); TacTerm s ] ] ; diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 33148ecea..6e2f5fe3a 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -81,11 +81,8 @@ let mlexpr_of_grammar_production = function let mlexpr_of_clause = mlexpr_of_list - (fun (a,b,c) -> - (mlexpr_of_pair - mlexpr_of_string - (mlexpr_of_list mlexpr_of_grammar_production) - (a,b))) + (fun (a,b,c) -> + mlexpr_of_list mlexpr_of_grammar_production (VernacTerm a::b)) let declare_command loc s cl = let gl = mlexpr_of_clause cl in diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 7ee45f67d..3eccf3d34 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -187,7 +187,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* For syntax extensions *) | TacAlias of loc * string * (identifier * ('constr,'tac) generic_argument) list - * (dir_path * 'tac) + * (dir_path * glob_tactic_expr) and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr @@ -230,6 +230,16 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg = | TacFreshId of string option | Tacexp of 'tac +(* Globalized tactics *) +and glob_tactic_expr = + (rawconstr_and_expr, + constr_pattern, + evaluable_global_reference and_short_name or_var, + inductive or_var, + ltac_constant located or_var, + identifier located, + glob_tactic_expr) gen_tactic_expr + type raw_tactic_expr = (constr_expr, pattern_expr, @@ -262,16 +272,6 @@ type raw_generic_argument = type raw_red_expr = (constr_expr, reference) red_expr_gen -(* Globalized tactics *) -type glob_tactic_expr = - (rawconstr_and_expr, - constr_pattern, - evaluable_global_reference and_short_name or_var, - inductive or_var, - ltac_constant located or_var, - identifier located, - glob_tactic_expr) gen_tactic_expr - type glob_atomic_tactic_expr = (rawconstr_and_expr, constr_pattern, diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 16dcc65ea..2f541b40d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -763,7 +763,7 @@ let rec intern_atomic lf ist x = let (l1,l2) = ist.ltacvars in let ist' = { ist with ltacvars = ((List.map fst l)@l1,l2) } in let l = List.map (fun (id,a) -> (strip_meta id,intern_genarg ist a)) l in - try TacAlias (loc,s,l,(dir,intern_tactic ist' body)) + try TacAlias (loc,s,l,(dir,body)) with e -> raise (locate_error_in_file (string_of_dirpath dir) e) and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr) @@ -902,8 +902,9 @@ and intern_genarg ist x = (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x)) | RedExprArgType -> in_gen globwit_red_expr (intern_redexp ist (out_gen rawwit_red_expr x)) - | TacticArgType -> - in_gen globwit_tactic (intern_tactic ist (out_gen rawwit_tactic x)) + | TacticArgType n -> + in_gen (globwit_tactic n) (intern_tactic ist + (out_gen (rawwit_tactic n) x)) | OpenConstrArgType b -> in_gen (globwit_open_constr_gen b) ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x))) @@ -1610,7 +1611,7 @@ and interp_genarg ist goal x = (out_gen globwit_quant_hyp x)) | RedExprArgType -> in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x)) - | TacticArgType -> in_gen wit_tactic (out_gen globwit_tactic x) + | TacticArgType n -> in_gen (wit_tactic n) (out_gen (globwit_tactic n) x) | OpenConstrArgType casted -> in_gen (wit_open_constr_gen casted) (pf_interp_open_constr casted ist goal @@ -1823,8 +1824,8 @@ and interp_atomic ist gl = function | ConstrMayEvalArgType -> VConstr (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x)) - | TacticArgType -> - val_interp ist gl (out_gen globwit_tactic x) + | TacticArgType n -> + val_interp ist gl (out_gen (globwit_tactic n) x) | StringArgType | BoolArgType | QuantHypArgType | RedExprArgType | OpenConstrArgType _ | ConstrWithBindingsArgType | BindingsArgType @@ -1833,7 +1834,9 @@ and interp_atomic ist gl = function in let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in let v = locate_tactic_call loc (val_interp { ist with lfun=lfun } gl body) - in tactic_of_value v gl + in + try tactic_of_value v gl + with NotTactic -> user_err_loc (loc,"",str "not a tactic") (* Initial call for interpretation *) let interp_tac_gen lfun debug t gl = @@ -2123,8 +2126,9 @@ and subst_genarg subst (x:glob_generic_argument) = (out_gen globwit_quant_hyp x)) | RedExprArgType -> in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x)) - | TacticArgType -> - in_gen globwit_tactic (subst_tactic subst (out_gen globwit_tactic x)) + | TacticArgType n -> + in_gen (globwit_tactic n) + (subst_tactic subst (out_gen (globwit_tactic n) x)) | OpenConstrArgType b -> in_gen (globwit_open_constr_gen b) ((),subst_rawconstr subst (snd (out_gen (globwit_open_constr_gen b) x))) diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 6207e2c69..89a319f09 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -56,4 +56,3 @@ Ltac f_equal := cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[do 5 des; r|r]|r]|r]|r]|r] | _ => idtac end. - diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 71a35edcc..a58c6f54c 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -144,19 +144,19 @@ let qualified_nterm current_univ = function | NtQual (univ, en) -> (univ, en) | NtShort en -> (current_univ, en) -let rec make_tags = function - | VTerm s :: l -> make_tags l +let rec make_tags lev = function + | VTerm s :: l -> make_tags lev l | VNonTerm (loc, nt, po) :: l -> let (u,nt) = qualified_nterm "tactic" nt in - let (etyp, _) = Egrammar.interp_entry_name u nt in - etyp :: make_tags l + let (etyp, _) = Egrammar.interp_entry_name lev u nt in + etyp :: make_tags lev l | [] -> [] let declare_pprule = function (* Pretty-printing rules only for Grammar (Tactic Notation) *) - | Egrammar.TacticGrammar gl -> - let f (s,(s',l),tac) = - let pp = (make_tags l, (s',List.map make_terminal_status l)) in + | Egrammar.TacticGrammar (n,gl) -> + let f (s,l,tac) = + let pp = (make_tags n l, (n,List.map make_terminal_status l)) in Pptactic.declare_extra_tactic_pprule true s pp; Pptactic.declare_extra_tactic_pprule false s pp in List.iter f gl @@ -166,8 +166,19 @@ let cache_grammar (_,a) = Egrammar.extend_grammar a; declare_pprule a +let subst_tactic_grammar subst (s,p,(d,tac)) = + (s,p,(d,Tacinterp.subst_tactic subst tac)) + +open Egrammar + let subst_grammar (_,subst,a) = - Egrammar.subst_all_grammar_command subst a + match a with + | Notation _ -> + anomaly "Notation not in GRAMMAR summary" + | Grammar gc -> + Grammar (subst_grammar_command subst gc) + | TacticGrammar (n,g) -> + TacticGrammar (n,List.map (subst_tactic_grammar subst) g) let (inGrammar, outGrammar) = declare_object {(default_object "GRAMMAR") with @@ -203,15 +214,15 @@ let cons_production_parameter l = function | VTerm _ -> l | VNonTerm (_,_,ido) -> option_cons ido l -let locate_tactic_body dir (s,(_,prods as p),e) = +let locate_tactic_body dir (s,prods,e) = let ids = List.fold_left cons_production_parameter [] prods in let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in - (s,p,(dir,tac)) + (s,prods,(dir,tac)) -let add_tactic_grammar g = +let add_tactic_grammar (n,g) = let dir = Lib.cwd () in let g = List.map (locate_tactic_body dir) g in - Lib.add_anonymous_leaf (inGrammar (Egrammar.TacticGrammar g)) + Lib.add_anonymous_leaf (inGrammar (Egrammar.TacticGrammar (n,g))) (* Printing grammar entries *) @@ -235,7 +246,10 @@ let print_grammar univ entry = | "pattern" -> Gram.Entry.print Pcoq.Constr.pattern | "tactic" -> - Gram.Entry.print Pcoq.Tactic.simple_tactic + msgnl (str "Entry tactic_expr is"); + Gram.Entry.print Pcoq.Tactic.tactic_expr; + msgnl (str "Entry simple_tactic is"); + Gram.Entry.print Pcoq.Tactic.simple_tactic; | _ -> error "Unknown or unprintable grammar entry" (* Parse a format (every terminal starting with a letter or a single diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index e9f41ac87..243b6345f 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -25,8 +25,8 @@ val add_syntax_obj : string -> raw_syntax_entry list -> unit val add_grammar_obj : string -> raw_grammar_entry list -> unit val add_token_obj : string -> unit -val add_tactic_grammar : - (string * (string * grammar_production list) * raw_tactic_expr) list -> unit +val add_tactic_grammar : + int * (string * grammar_production list * raw_tactic_expr) list -> unit val add_infix : locality_flag -> (string * syntax_modifier list) -> reference -> (string * syntax_modifier list) option -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7d791dd74..b65379d65 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1072,7 +1072,7 @@ let interp c = match c with (* Syntax *) | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel - | VernacTacticGrammar al -> Metasyntax.add_tactic_grammar al + | VernacTacticGrammar (n,al) -> Metasyntax.add_tactic_grammar (n,al) | VernacGrammar (univ,al) -> vernac_grammar univ al | VernacSyntaxExtension (lcl,sl,l8) -> vernac_syntax_extension lcl sl l8 | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 0d54fb66d..8c1d77511 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -171,8 +171,8 @@ type vernac_expr = (* Syntax *) | VernacGrammar of lstring * raw_grammar_entry list - | VernacTacticGrammar of - (lstring * (lstring * grammar_production list) * raw_tactic_expr) list + | VernacTacticGrammar of int * + (lstring * grammar_production list * raw_tactic_expr) list | VernacSyntax of lstring * raw_syntax_entry list | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list) option diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 141ae1cbe..c7b01607f 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -386,10 +386,24 @@ let rec pr_tacarg_using_rule pr_gen = function let pr_then () = str ";" +let ltop = (5,E) +let lseq = 5 +let ltactical = 3 +let lorelse = 2 +let llet = 1 +let lfun = 1 +let labstract = 3 +let lmatch = 1 +let latom = 0 +let lcall = 1 +let leval = 1 +let ltatom = 1 + +let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq open Closure -let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders) = +let make_pr_tac (pr_tac_level,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders) = let pr_bindings env = pr_bindings (pr_lconstr env) (pr_constr env) in let pr_ex_bindings env = pr_bindings_gen true (pr_lconstr env) (pr_constr env) in @@ -467,10 +481,10 @@ and pr_atom1 env = function errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0") | TacExtend (loc,s,l) -> pr_with_comments loc - (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s l) + (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac_level env) 1 s l) | TacAlias (loc,s,l,_) -> pr_with_comments loc - (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s + (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac_level env) 1 s (List.map snd l)) (* Basic tactics *) @@ -633,7 +647,7 @@ and pr_atom1 env = function | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings env l) | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings env l) | TacAnyConstructor (Some t) -> - hov 1 (str "constructor" ++ pr_arg (pr_tac0 env) t) + hov 1 (str "constructor" ++ pr_arg (pr_tac_level env (latom,E)) t) | TacAnyConstructor None as t -> pr_atom0 env t | TacConstructor (n,l) -> hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++ @@ -676,19 +690,6 @@ and pr_atom1 env = function in -let ltop = (5,E) in -let lseq = 5 in -let ltactical = 3 in -let lorelse = 2 in -let llet = 1 in -let lfun = 1 in -let labstract = 3 in -let lmatch = 1 in -let latom = 0 in -let lcall = 1 in -let leval = 1 in -let ltatom = 1 in - let rec pr_tac env inherited tac = let (strm,prec) = match tac with | TacAbstract (t,None) -> @@ -791,9 +792,14 @@ let rec pr_tac env inherited tac = str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet | TacId "" -> str "idtac", latom | TacId s -> str "idtac" ++ (qsnew s), latom + | TacAtom (loc,TacAlias (_,s,l,_)) -> + pr_with_comments loc + (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac_level env) + (level_of inherited) s + (List.map snd l)), latom | TacAtom (loc,t) -> pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom - | TacArg(Tacexp e) -> pr_tac0 env e, latom + | TacArg(Tacexp e) -> pr_tac_level env (latom,E) e, latom | TacArg(ConstrMayEval (ConstrTerm c)) -> str "constr:" ++ pr_constr env c, latom | TacArg(ConstrMayEval c) -> @@ -826,13 +832,7 @@ and pr_tacarg env = function | (TacCall _|Tacexp _|Integer _) as a -> str "ltac:" ++ pr_tac env (latom,E) (TacArg a) -in ((fun env -> pr_tac env ltop), - (fun env -> pr_tac env (latom,E)), - pr_match_rule) - -let pi1 (a,_,_) = a -let pi2 (_,a,_) = a -let pi3 (_,_,a) = a +in (pr_tac, pr_match_rule) let strip_prod_binders_rawterm n (ty,_) = let rec strip_ty acc n ty = @@ -852,10 +852,8 @@ let strip_prod_binders_constr n ty = | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty - let rec raw_printers = - (pr_raw_tactic, - pr_raw_tactic0, + (pr_raw_tactic_level, Ppconstrnew.pr_constr_env, Ppconstrnew.pr_lconstr_env, Ppconstrnew.pr_pattern, @@ -866,21 +864,17 @@ let rec raw_printers = Pptactic.pr_raw_extend, strip_prod_binders_expr) -and pr_raw_tactic env (t:raw_tactic_expr) = - pi1 (make_pr_tac raw_printers) env t - -and pr_raw_tactic0 env t = - pi2 (make_pr_tac raw_printers) env t +and pr_raw_tactic_level env n (t:raw_tactic_expr) = + fst (make_pr_tac raw_printers) env n t and pr_raw_match_rule env t = - pi3 (make_pr_tac raw_printers) env t + snd (make_pr_tac raw_printers) env t let pr_and_constr_expr pr (c,_) = pr c let rec glob_printers = - (pr_glob_tactic, - pr_glob_tactic0, + (pr_glob_tactic_level, (fun env -> pr_and_constr_expr (Ppconstrnew.pr_rawconstr_env_no_translate env)), (fun env -> pr_and_constr_expr (Ppconstrnew.pr_lrawconstr_env_no_translate env)), (fun c -> Ppconstrnew.pr_constr_pattern_env (Global.env()) c), @@ -891,19 +885,15 @@ let rec glob_printers = Pptactic.pr_glob_extend, strip_prod_binders_rawterm) -and pr_glob_tactic env (t:glob_tactic_expr) = - pi1 (make_pr_tac glob_printers) env t - -and pr_glob_tactic0 env t = - pi2 (make_pr_tac glob_printers) env t +and pr_glob_tactic_level env n (t:glob_tactic_expr) = + fst (make_pr_tac glob_printers) env n t and pr_glob_match_rule env t = - pi3 (make_pr_tac glob_printers) env t + snd (make_pr_tac glob_printers) env t -let (pr_tactic,_,_) = +let ((pr_tactic_level:env -> tolerability -> Proof_type.tactic_expr -> std_ppcmds),_) = make_pr_tac - (pr_glob_tactic, - pr_glob_tactic0, + (pr_glob_tactic_level, pr_term_env, pr_lterm_env, Ppconstrnew.pr_constr_pattern, @@ -914,6 +904,10 @@ let (pr_tactic,_,_) = Pptactic.pr_extend, strip_prod_binders_constr) +let pr_raw_tactic env = pr_raw_tactic_level env ltop +let pr_glob_tactic env = pr_glob_tactic_level env ltop +let pr_tactic env = pr_tactic_level env ltop + let _ = Tactic_debug.set_tactic_printer (fun x -> if !Options.v7 then Pptactic.pr_glob_tactic x diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli index b2e8942ad..3dafb3615 100644 --- a/translate/pptacticnew.mli +++ b/translate/pptacticnew.mli @@ -14,15 +14,19 @@ open Tacexpr open Proof_type open Topconstr open Names +open Environ +open Ppextend val qsnew : string -> std_ppcmds val pr_intro_pattern : intro_pattern_expr -> std_ppcmds -val pr_raw_tactic : Environ.env -> raw_tactic_expr -> std_ppcmds +val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds + +val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds -val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds +val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds -val pr_tactic : Environ.env -> Proof_type.tactic_expr -> std_ppcmds +val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds val id_of_ltac_v7_id : identifier -> identifier diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 985280cfd..86f20bb6f 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -91,7 +91,7 @@ let pr_raw_tactic_env l env t = let pr_gen env t = Pptactic.pr_raw_generic (Ppconstrnew.pr_constr_env env) (Ppconstrnew.pr_lconstr_env env) - (Pptacticnew.pr_raw_tactic env) pr_reference t + (Pptacticnew.pr_raw_tactic_level env) pr_reference t let pr_raw_tactic tac = Pptacticnew.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic tac) @@ -103,8 +103,8 @@ let rec extract_signature = function let rec match_vernac_rule tys = function [] -> raise Not_found - | (s,pargs)::rls -> - if extract_signature pargs = tys then (s,pargs) + | pargs::rls -> + if extract_signature pargs = tys then pargs else match_vernac_rule tys rls let sep = fun _ -> spc() @@ -400,16 +400,12 @@ let pr_syntax_modifiers = function | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") -let pr_grammar_tactic_rule (name,(s,pil),t) = -(* - hov 0 ( - (* str name ++ spc() ++ *) - hov 0 (str"[" ++ qsnew s ++ spc() ++ - prlist_with_sep sep pr_production_item pil ++ str"]") ++ - spc() ++ hov 0 (str"->" ++ spc() ++ str"[" ++ pr_raw_tactic t ++ str"]")) -*) - hov 2 (str "Tactic Notation" ++ spc() ++ - hov 0 (qsnew s ++ spc() ++ prlist_with_sep sep pr_production_item pil ++ +let print_level n = + if n <> 0 then str " (at level " ++ int n ++ str ")" else mt () + +let pr_grammar_tactic_rule n (name,pil,t) = + hov 2 (str "Tactic Notation" ++ print_level n ++ spc() ++ + hov 0 (prlist_with_sep sep pr_production_item pil ++ spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) let pr_box b = let pr_boxkind = function @@ -526,11 +522,9 @@ let rec pr_vernac = function | VernacGrammar _ -> msgerrnl (str"Warning : constr Grammar is discontinued; use Notation"); str"(* <Warning> : Grammar is replaced by Notation *)" - | VernacTacticGrammar l -> - prlist_with_sep (fun () -> sep_end() ++ fnl()) pr_grammar_tactic_rule l -(* - hov 1 (str"Grammar tactic simple_tactic :=" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_grammar_tactic_rule l) (***) -*) + | VernacTacticGrammar (n,l) -> + prlist_with_sep (fun () -> sep_end() ++ fnl()) + (pr_grammar_tactic_rule n) l | VernacSyntax (u,el) -> msgerrnl (str"Warning : Syntax is discontinued; use Notation"); str"(* <Warning> : Syntax is discontinued" ++ @@ -1095,7 +1089,7 @@ and pr_extend s cl = | "HintRewriteV8", [a;b;c;d] -> [a;b;d;c] | _ -> cl in let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in - let (hd,rl) = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in + let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in let (pp,_) = List.fold_left (fun (strm,args) pi -> @@ -1104,7 +1098,7 @@ and pr_extend s cl = (strm ++ pr_gen (Global.env()) (List.hd args), List.tl args) | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args)) - (str hd,cl) rl in + (mt(),cl) rl in hov 1 pp ++ (if s = "Correctness" then sep_end () ++ fnl() ++ str "Proof" else mt()) with Not_found -> |