From 29c67f1d97221755415ace1e4317cb7af92e24f3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 29 May 2002 11:10:24 +0000 Subject: Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 1679 +++++++++++++++++++++--------------- .depend.camlp4 | 18 +- .depend.coq | 11 +- CHANGES | 36 +- Makefile | 178 ++-- TODO | 36 +- contrib/correctness/pcic.ml | 2 +- contrib/correctness/ptactic.ml | 20 +- contrib/extraction/Extraction.v | 86 -- contrib/extraction/extract_env.ml | 119 ++- contrib/extraction/extract_env.mli | 9 + contrib/extraction/table.ml | 84 +- contrib/extraction/table.mli | 17 +- contrib/fourier/fourierR.ml | 6 +- contrib/omega/coq_omega.ml | 49 +- contrib/ring/quote.ml | 14 +- contrib/ring/ring.ml | 198 +---- contrib/romega/refl_omega.ml | 5 + contrib/xml/xmlcommand.mli | 4 +- dev/changements.txt | 42 + dev/db_printers.ml | 2 +- dev/top_printers.ml | 2 +- doc/newsyntax.tex | 6 + parsing/extend.ml4 | 303 ------- scripts/coqmktop.ml | 10 +- states/MakeInitial.v | 8 - syntax/MakeBare.v | 1 - tactics/tacentries.ml | 58 -- tactics/tacentries.mli | 55 -- tools/coq_makefile.ml4 | 8 +- 30 files changed, 1421 insertions(+), 1645 deletions(-) delete mode 100644 contrib/extraction/Extraction.v delete mode 100644 parsing/extend.ml4 delete mode 100644 tactics/tacentries.ml delete mode 100644 tactics/tacentries.mli diff --git a/.depend b/.depend index f29e747938..1dd798f9a6 100644 --- a/.depend +++ b/.depend @@ -33,13 +33,13 @@ library/global.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/indtypes.cmi kernel/names.cmi library/nametab.cmi \ kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi library/goptions.cmi: kernel/names.cmi library/nametab.cmi lib/pp.cmi \ - kernel/term.cmi + kernel/term.cmi lib/util.cmi library/impargs.cmi: kernel/environ.cmi kernel/names.cmi library/nametab.cmi \ kernel/term.cmi library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi library/libobject.cmi: kernel/names.cmi library/library.cmi: library/lib.cmi library/libobject.cmi kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi lib/system.cmi + library/nametab.cmi lib/pp.cmi lib/system.cmi lib/util.cmi library/nameops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/term.cmi library/nametab.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ @@ -48,33 +48,44 @@ library/summary.cmi: kernel/names.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 kernel/names.cmi \ - parsing/pcoq.cmi lib/pp.cmi +parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \ + kernel/names.cmi library/nametab.cmi lib/pp.cmi proofs/tacexpr.cmo \ + lib/util.cmi parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \ library/impargs.cmi kernel/names.cmi library/nametab.cmi \ pretyping/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \ - kernel/term.cmi + kernel/term.cmi lib/util.cmi parsing/coqast.cmi: lib/dyn.cmi kernel/names.cmi parsing/coqlib.cmi: kernel/names.cmi library/nametab.cmi \ pretyping/pattern.cmi kernel/term.cmi parsing/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ - parsing/pcoq.cmi + parsing/genarg.cmi proofs/tacexpr.cmo toplevel/vernacexpr.cmo parsing/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ + kernel/names.cmi lib/pp.cmi toplevel/vernacexpr.cmo +parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi library/nametab.cmi \ lib/pp.cmi -parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ - lib/pp.cmi +parsing/genarg.cmi: kernel/closure.cmi parsing/coqast.cmi pretyping/evd.cmi \ + kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \ + kernel/term.cmi lib/util.cmi parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/term.cmi parsing/g_zsyntax.cmi: parsing/coqast.cmi -parsing/pcoq.cmi: parsing/coqast.cmi +parsing/pcoq.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \ + kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \ + proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo +parsing/ppconstr.cmi: parsing/coqast.cmi kernel/environ.cmi \ + parsing/extend.cmi parsing/genarg.cmi library/nametab.cmi \ + parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \ + kernel/term.cmi +parsing/pptactic.cmi: parsing/egrammar.cmi parsing/genarg.cmi lib/pp.cmi \ + proofs/proof_type.cmi proofs/tacexpr.cmo parsing/prettyp.cmi: pretyping/classops.cmi kernel/environ.cmi \ library/lib.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/sign.cmi \ + kernel/term.cmi pretyping/termops.cmi lib/util.cmi +parsing/printer.cmi: kernel/environ.cmi kernel/names.cmi library/nametab.cmi \ + pretyping/pattern.cmi lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi \ kernel/term.cmi pretyping/termops.cmi -parsing/printer.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \ - library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \ - pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \ - pretyping/termops.cmi parsing/search.cmi: kernel/environ.cmi kernel/names.cmi library/nametab.cmi \ pretyping/pattern.cmi lib/pp.cmi kernel/term.cmi parsing/termast.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \ @@ -129,75 +140,91 @@ pretyping/retyping.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ pretyping/syntax_def.cmi: kernel/names.cmi library/nametab.cmi \ pretyping/rawterm.cmi pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi pretyping/evd.cmi \ - kernel/names.cmi pretyping/reductionops.cmi kernel/term.cmi + kernel/names.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \ + kernel/term.cmi pretyping/termops.cmi: kernel/environ.cmi kernel/names.cmi \ library/nametab.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \ kernel/univ.cmi lib/util.cmi pretyping/typing.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/term.cmi proofs/clenv.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \ pretyping/evd.cmi kernel/names.cmi lib/pp.cmi pretyping/pretyping.cmi \ - proofs/proof_type.cmi pretyping/reductionops.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi lib/util.cmi + proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \ + kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi proofs/evar_refiner.cmi: parsing/coqast.cmi kernel/environ.cmi \ pretyping/evd.cmi kernel/names.cmi proofs/proof_type.cmi \ proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi proofs/logic.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi -proofs/pfedit.cmi: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ - pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ +proofs/pfedit.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \ + kernel/names.cmi library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi \ kernel/safe_typing.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi -proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi \ - pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ - kernel/sign.cmi kernel/term.cmi lib/util.cmi -proofs/proof_type.cmi: parsing/coqast.cmi kernel/environ.cmi \ - pretyping/evd.cmi kernel/names.cmi library/nametab.cmi \ - pretyping/pretyping.cmi pretyping/tacred.cmi kernel/term.cmi lib/util.cmi +proofs/proof_trees.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ + lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi \ + lib/util.cmi +proofs/proof_type.cmi: kernel/closure.cmi kernel/environ.cmi \ + pretyping/evd.cmi parsing/genarg.cmi kernel/names.cmi library/nametab.cmi \ + pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi lib/util.cmi proofs/refiner.cmi: pretyping/evd.cmi lib/pp.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi -proofs/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \ - pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ - proofs/tacmach.cmi proofs/tactic_debug.cmi kernel/term.cmi + proofs/proof_type.cmi kernel/sign.cmi proofs/tacexpr.cmo kernel/term.cmi proofs/tacmach.cmi: kernel/closure.cmi parsing/coqast.cmi kernel/environ.cmi \ - pretyping/evd.cmi kernel/names.cmi lib/pp.cmi pretyping/pretyping.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \ - proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi -proofs/tactic_debug.cmi: parsing/coqast.cmi kernel/environ.cmi \ - proofs/proof_type.cmi kernel/term.cmi -tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi parsing/coqast.cmi \ - kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi library/nametab.cmi \ + pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ + proofs/refiner.cmi kernel/sign.cmi proofs/tacexpr.cmo \ + pretyping/tacred.cmi kernel/term.cmi +proofs/tactic_debug.cmi: kernel/environ.cmi kernel/names.cmi \ + proofs/proof_type.cmi proofs/tacexpr.cmo kernel/term.cmi +tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi kernel/environ.cmi \ + pretyping/evd.cmi kernel/names.cmi library/nametab.cmi \ pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ - pretyping/rawterm.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ - lib/util.cmi -tactics/autorewrite.cmi: parsing/coqast.cmi proofs/tacmach.cmi \ + pretyping/rawterm.cmi kernel/sign.cmi proofs/tacexpr.cmo \ + proofs/tacmach.cmi kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo +tactics/autorewrite.cmi: proofs/tacexpr.cmo proofs/tacmach.cmi \ kernel/term.cmi tactics/btermdn.cmi: pretyping/pattern.cmi kernel/term.cmi -tactics/dhyp.cmi: kernel/names.cmi proofs/tacmach.cmi -tactics/elim.cmi: kernel/names.cmi proofs/proof_type.cmi proofs/tacmach.cmi \ +tactics/contradiction.cmi: kernel/names.cmi proofs/proof_type.cmi \ + kernel/term.cmi +tactics/dhyp.cmi: parsing/genarg.cmi kernel/names.cmi proofs/tacexpr.cmo \ + proofs/tacmach.cmi +tactics/elim.cmi: kernel/names.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ tactics/tacticals.cmi kernel/term.cmi tactics/equality.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \ tactics/hipattern.cmi kernel/names.cmi pretyping/pattern.cmi \ - proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - tactics/wcclausenv.cmi + proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \ + proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi tactics/wcclausenv.cmi +tactics/extraargs.cmi: parsing/coqast.cmi parsing/pcoq.cmi \ + proofs/proof_type.cmi proofs/tacexpr.cmo kernel/term.cmi +tactics/extratactics.cmi: parsing/genarg.cmi kernel/names.cmi \ + proofs/proof_type.cmi kernel/term.cmi tactics/hiddentac.cmi: kernel/names.cmi proofs/proof_type.cmi \ - tactics/tacentries.cmi proofs/tacmach.cmi kernel/term.cmi + pretyping/rawterm.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ + pretyping/tacred.cmi kernel/term.cmi tactics/hipattern.cmi: pretyping/evd.cmi kernel/names.cmi \ pretyping/pattern.cmi proofs/proof_trees.cmi kernel/sign.cmi \ kernel/term.cmi lib/util.cmi -tactics/inv.cmi: kernel/names.cmi proofs/tacmach.cmi kernel/term.cmi +tactics/inv.cmi: kernel/names.cmi pretyping/rawterm.cmi proofs/tacmach.cmi \ + kernel/term.cmi +tactics/leminv.cmi: parsing/coqast.cmi kernel/names.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi kernel/term.cmi tactics/nbtermdn.cmi: tactics/btermdn.cmi pretyping/pattern.cmi \ kernel/term.cmi tactics/refine.cmi: pretyping/pretyping.cmi proofs/tacmach.cmi \ kernel/term.cmi -tactics/setoid_replace.cmi: proofs/proof_type.cmi kernel/term.cmi -tactics/tacentries.cmi: proofs/proof_type.cmi proofs/tacmach.cmi -tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \ +tactics/setoid_replace.cmi: parsing/genarg.cmi kernel/names.cmi \ + proofs/proof_type.cmi kernel/term.cmi +tactics/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \ + pretyping/evd.cmi parsing/genarg.cmi kernel/names.cmi lib/pp.cmi \ + proofs/proof_type.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ + pretyping/tacred.cmi proofs/tactic_debug.cmi kernel/term.cmi lib/util.cmi +tactics/tacticals.cmi: proofs/clenv.cmi kernel/names.cmi \ pretyping/pattern.cmi proofs/proof_type.cmi kernel/reduction.cmi \ kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi -tactics/tactics.cmi: proofs/clenv.cmi kernel/closure.cmi kernel/environ.cmi \ - proofs/evar_refiner.cmi pretyping/evd.cmi kernel/names.cmi \ - library/nametab.cmi proofs/proof_type.cmi kernel/reduction.cmi \ - kernel/sign.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ +tactics/tactics.cmi: proofs/clenv.cmi kernel/closure.cmi parsing/coqast.cmi \ + kernel/environ.cmi proofs/evar_refiner.cmi pretyping/evd.cmi \ + kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \ + proofs/tacexpr.cmo proofs/tacmach.cmi pretyping/tacred.cmi \ tactics/tacticals.cmi kernel/term.cmi tactics/termdn.cmi: pretyping/pattern.cmi kernel/term.cmi tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi \ @@ -205,11 +232,12 @@ tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi \ proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi toplevel/cerrors.cmi: parsing/coqast.cmi lib/pp.cmi toplevel/class.cmi: pretyping/classops.cmi library/declare.cmi \ - kernel/names.cmi library/nametab.cmi kernel/term.cmi -toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi \ - kernel/environ.cmi pretyping/evd.cmi kernel/indtypes.cmi \ - library/library.cmi kernel/names.cmi library/nametab.cmi \ - kernel/safe_typing.cmi pretyping/tacred.cmi kernel/term.cmi + kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \ + kernel/term.cmi +toplevel/command.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \ + kernel/indtypes.cmi library/library.cmi kernel/names.cmi \ + library/nametab.cmi proofs/proof_type.cmi pretyping/tacred.cmi \ + kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo toplevel/coqinit.cmi: kernel/names.cmi toplevel/discharge.cmi: kernel/names.cmi toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ @@ -217,20 +245,23 @@ toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ toplevel/himsg.cmi: pretyping/cases.cmi kernel/environ.cmi \ kernel/indtypes.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \ pretyping/pretype_errors.cmi kernel/type_errors.cmi -toplevel/metasyntax.cmi: parsing/coqast.cmi +toplevel/metasyntax.cmi: parsing/coqast.cmi parsing/extend.cmi \ + library/nametab.cmi proofs/tacexpr.cmo lib/util.cmi \ + toplevel/vernacexpr.cmo toplevel/mltop.cmi: library/libobject.cmi kernel/names.cmi toplevel/protectedtoplevel.cmi: lib/pp.cmi -toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/sign.cmi \ - kernel/term.cmi -toplevel/recordobj.cmi: library/nametab.cmi +toplevel/record.cmi: parsing/genarg.cmi kernel/names.cmi kernel/sign.cmi \ + kernel/term.cmi toplevel/vernacexpr.cmo +toplevel/recordobj.cmi: library/nametab.cmi proofs/proof_type.cmi toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi -toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ - kernel/names.cmi kernel/term.cmi toplevel/vernacinterp.cmi -toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ - library/nametab.cmi proofs/proof_type.cmi -toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi +toplevel/vernacentries.cmi: parsing/coqast.cmi kernel/environ.cmi \ + pretyping/evd.cmi kernel/names.cmi library/nametab.cmi kernel/term.cmi \ + lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi +toplevel/vernacinterp.cmi: proofs/tacexpr.cmo +toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi \ + toplevel/vernacexpr.cmo contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \ contrib/correctness/ptype.cmi kernel/term.cmi contrib/correctness/pcicenv.cmi: kernel/names.cmi \ @@ -278,6 +309,8 @@ contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \ contrib/extraction/common.cmi: contrib/extraction/miniml.cmi \ contrib/extraction/mlutil.cmi kernel/names.cmi library/nametab.cmi \ lib/pp.cmi +contrib/extraction/extract_env.cmi: parsing/genarg.cmi kernel/names.cmi \ + library/nametab.cmi lib/util.cmi contrib/extraction/extraction.cmi: kernel/environ.cmi \ contrib/extraction/miniml.cmi kernel/names.cmi library/nametab.cmi \ kernel/term.cmi @@ -291,16 +324,17 @@ contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \ library/nametab.cmi lib/pp.cmi contrib/extraction/table.cmi \ kernel/term.cmi contrib/extraction/table.cmi: kernel/names.cmi library/nametab.cmi \ - toplevel/vernacinterp.cmi -contrib/interface/blast.cmi: contrib/interface/ctast.cmo \ - proofs/proof_type.cmi proofs/tacmach.cmi -contrib/interface/dad.cmi: contrib/interface/ctast.cmo proofs/proof_type.cmi \ - proofs/tacmach.cmi -contrib/interface/debug_tac.cmi: parsing/coqast.cmi proofs/proof_type.cmi \ + lib/util.cmi toplevel/vernacinterp.cmi +contrib/interface/blast.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \ proofs/tacmach.cmi -contrib/interface/name_to_ast.cmi: parsing/coqast.cmi library/nametab.cmi -contrib/interface/pbp.cmi: contrib/interface/ctast.cmo proofs/proof_type.cmi \ +contrib/interface/dad.cmi: contrib/interface/ctast.cmo proofs/proof_type.cmi \ + proofs/tacexpr.cmo proofs/tacmach.cmi +contrib/interface/debug_tac.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \ proofs/tacmach.cmi +contrib/interface/name_to_ast.cmi: parsing/coqast.cmi library/nametab.cmi \ + toplevel/vernacexpr.cmo +contrib/interface/pbp.cmi: kernel/names.cmi proofs/proof_type.cmi \ + proofs/tacexpr.cmo proofs/tacmach.cmi contrib/interface/showproof.cmi: contrib/interface/ascent.cmi \ parsing/astterm.cmi proofs/clenv.cmi parsing/coqast.cmi \ kernel/declarations.cmi kernel/environ.cmi pretyping/evd.cmi \ @@ -314,26 +348,29 @@ contrib/interface/translate.cmi: contrib/interface/ascent.cmi \ kernel/term.cmi contrib/interface/vtp.cmi: contrib/interface/ascent.cmi contrib/interface/xlate.cmi: contrib/interface/ascent.cmi \ - contrib/interface/ctast.cmo + contrib/interface/ctast.cmo kernel/names.cmi proofs/tacexpr.cmo \ + toplevel/vernacexpr.cmo contrib/jprover/jall.cmi: contrib/jprover/jlogic.cmi \ contrib/jprover/jterm.cmi contrib/jprover/opname.cmi contrib/jprover/jlogic.cmi: contrib/jprover/jterm.cmi contrib/jprover/jterm.cmi: contrib/jprover/opname.cmi -contrib/xml/xmlcommand.cmi: kernel/names.cmi library/nametab.cmi +contrib/xml/xmlcommand.cmi: kernel/names.cmi library/nametab.cmi lib/util.cmi config/coq_config.cmo: config/coq_config.cmi config/coq_config.cmx: config/coq_config.cmi dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi dev/db_printers.cmx: kernel/names.cmx lib/pp.cmx dev/top_printers.cmo: parsing/ast.cmi toplevel/cerrors.cmi proofs/clenv.cmi \ kernel/environ.cmi pretyping/evd.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ - proofs/refiner.cmi kernel/sign.cmi lib/system.cmi proofs/tacmach.cmi \ - kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi kernel/univ.cmi + library/nametab.cmi lib/pp.cmi parsing/pptactic.cmi parsing/printer.cmi \ + proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi lib/system.cmi \ + proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \ + pretyping/termops.cmi kernel/univ.cmi dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \ kernel/environ.cmx pretyping/evd.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ - proofs/refiner.cmx kernel/sign.cmx lib/system.cmx proofs/tacmach.cmx \ - kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx kernel/univ.cmx + library/nametab.cmx lib/pp.cmx parsing/pptactic.cmx parsing/printer.cmx \ + proofs/proof_trees.cmx proofs/refiner.cmx kernel/sign.cmx lib/system.cmx \ + proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \ + pretyping/termops.cmx kernel/univ.cmx kernel/closure.cmo: kernel/environ.cmi kernel/esubst.cmi kernel/names.cmi \ lib/pp.cmi kernel/term.cmi lib/util.cmi kernel/closure.cmi kernel/closure.cmx: kernel/environ.cmx kernel/esubst.cmx kernel/names.cmx \ @@ -534,10 +571,12 @@ lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi lib/util.cmo: lib/pp.cmi lib/util.cmi lib/util.cmx: lib/pp.cmx lib/util.cmi -parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ - parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi -parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \ - parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/ast.cmi +parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + proofs/tacexpr.cmo lib/util.cmi parsing/ast.cmi +parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx parsing/genarg.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + proofs/tacexpr.cmx lib/util.cmx parsing/ast.cmi parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ lib/dyn.cmi kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ library/global.cmi library/impargs.cmi library/nameops.cmi \ @@ -565,33 +604,51 @@ parsing/coqlib.cmo: library/declare.cmi kernel/names.cmi library/nametab.cmi \ parsing/coqlib.cmx: library/declare.cmx kernel/names.cmx library/nametab.cmx \ pretyping/pattern.cmx kernel/term.cmx lib/util.cmx parsing/coqlib.cmi parsing/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ - parsing/lexer.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi \ + parsing/genarg.cmi parsing/lexer.cmi parsing/pcoq.cmi lib/pp.cmi \ + proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo \ parsing/egrammar.cmi parsing/egrammar.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \ - parsing/lexer.cmx parsing/pcoq.cmx lib/pp.cmx lib/util.cmx \ + parsing/genarg.cmx parsing/lexer.cmx parsing/pcoq.cmx lib/pp.cmx \ + proofs/tacexpr.cmx lib/util.cmx toplevel/vernacexpr.cmx \ parsing/egrammar.cmi parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ - lib/gmap.cmi lib/gmapl.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \ - parsing/esyntax.cmi + parsing/genarg.cmi library/global.cmi lib/gmap.cmi lib/gmapl.cmi \ + kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \ + lib/util.cmi toplevel/vernacexpr.cmo parsing/esyntax.cmi parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \ - lib/gmap.cmx lib/gmapl.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ - parsing/esyntax.cmi -parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \ - parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi -parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \ - parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi -parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi -parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx + parsing/genarg.cmx library/global.cmx lib/gmap.cmx lib/gmapl.cmx \ + kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ + lib/util.cmx toplevel/vernacexpr.cmx parsing/esyntax.cmi +parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \ + parsing/lexer.cmi library/nametab.cmi lib/pp.cmi lib/util.cmi \ + parsing/extend.cmi +parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/genarg.cmx \ + parsing/lexer.cmx library/nametab.cmx lib/pp.cmx lib/util.cmx \ + parsing/extend.cmi +parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi \ + parsing/extend.cmi library/goptions.cmi parsing/pcoq.cmi lib/pp.cmi \ + toplevel/vernacexpr.cmo +parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx \ + parsing/extend.cmx library/goptions.cmx parsing/pcoq.cmx lib/pp.cmx \ + toplevel/vernacexpr.cmx parsing/g_cases.cmo: parsing/coqast.cmi kernel/names.cmi parsing/pcoq.cmi parsing/g_cases.cmx: parsing/coqast.cmx kernel/names.cmx parsing/pcoq.cmx parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \ parsing/pcoq.cmi parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx kernel/names.cmx \ parsing/pcoq.cmx -parsing/g_ltac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ - lib/pp.cmi lib/util.cmi -parsing/g_ltac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \ - lib/pp.cmx lib/util.cmx +parsing/genarg.cmo: parsing/coqast.cmi pretyping/evd.cmi kernel/names.cmi \ + library/nametab.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \ + parsing/genarg.cmi +parsing/genarg.cmx: parsing/coqast.cmx pretyping/evd.cmx kernel/names.cmx \ + library/nametab.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \ + parsing/genarg.cmi +parsing/g_ltac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \ + kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \ + proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo +parsing/g_ltac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/genarg.cmx \ + kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx \ + proofs/tacexpr.cmx lib/util.cmx toplevel/vernacexpr.cmx parsing/g_minicoq.cmo: kernel/environ.cmi parsing/lexer.cmi kernel/names.cmi \ lib/pp.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ parsing/g_minicoq.cmi @@ -599,43 +656,75 @@ parsing/g_minicoq.cmx: kernel/environ.cmx parsing/lexer.cmx kernel/names.cmx \ lib/pp.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ parsing/g_minicoq.cmi parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \ - parsing/coqlib.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \ - lib/pp.cmi parsing/termast.cmi lib/util.cmi parsing/g_natsyntax.cmi + parsing/coqlib.cmi parsing/esyntax.cmi parsing/extend.cmi \ + kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi parsing/termast.cmi \ + lib/util.cmi parsing/g_natsyntax.cmi parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \ - parsing/coqlib.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx \ - lib/pp.cmx parsing/termast.cmx lib/util.cmx parsing/g_natsyntax.cmi -parsing/g_prim.cmo: parsing/coqast.cmi kernel/names.cmi parsing/pcoq.cmi -parsing/g_prim.cmx: parsing/coqast.cmx kernel/names.cmx parsing/pcoq.cmx -parsing/g_proofs.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \ - lib/util.cmi -parsing/g_proofs.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \ - lib/util.cmx + parsing/coqlib.cmx parsing/esyntax.cmx parsing/extend.cmx \ + kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx parsing/termast.cmx \ + lib/util.cmx parsing/g_natsyntax.cmi +parsing/g_prim.cmo: parsing/coqast.cmi kernel/names.cmi library/nametab.cmi \ + parsing/pcoq.cmi proofs/tacexpr.cmo +parsing/g_prim.cmx: parsing/coqast.cmx kernel/names.cmx library/nametab.cmx \ + parsing/pcoq.cmx proofs/tacexpr.cmx +parsing/g_proofs.cmo: parsing/coqast.cmi parsing/genarg.cmi parsing/pcoq.cmi \ + lib/pp.cmi proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo +parsing/g_proofs.cmx: parsing/coqast.cmx parsing/genarg.cmx parsing/pcoq.cmx \ + lib/pp.cmx proofs/tacexpr.cmx lib/util.cmx toplevel/vernacexpr.cmx parsing/g_rsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \ - parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \ - lib/util.cmi -parsing/g_rsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \ - parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx \ - lib/util.cmx -parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ + parsing/esyntax.cmi parsing/extend.cmi kernel/names.cmi parsing/pcoq.cmi \ lib/pp.cmi lib/util.cmi -parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \ - lib/pp.cmx lib/util.cmx -parsing/g_vernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ - lib/pp.cmi lib/util.cmi -parsing/g_vernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \ +parsing/g_rsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \ + parsing/esyntax.cmx parsing/extend.cmx kernel/names.cmx parsing/pcoq.cmx \ lib/pp.cmx lib/util.cmx +parsing/g_tactic.cmo: parsing/ast.cmi parsing/genarg.cmi kernel/names.cmi \ + parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \ + lib/util.cmi +parsing/g_tactic.cmx: parsing/ast.cmx parsing/genarg.cmx kernel/names.cmx \ + parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \ + lib/util.cmx +parsing/g_vernac.cmo: parsing/ast.cmi toplevel/class.cmi parsing/coqast.cmi \ + library/declare.cmi parsing/genarg.cmi library/goptions.cmi \ + library/nametab.cmi lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \ + toplevel/recordobj.cmi lib/util.cmi toplevel/vernacexpr.cmo +parsing/g_vernac.cmx: parsing/ast.cmx toplevel/class.cmx parsing/coqast.cmx \ + library/declare.cmx parsing/genarg.cmx library/goptions.cmx \ + library/nametab.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \ + toplevel/recordobj.cmx lib/util.cmx toplevel/vernacexpr.cmx parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \ - parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \ - lib/util.cmi parsing/g_zsyntax.cmi + parsing/esyntax.cmi parsing/extend.cmi kernel/names.cmi parsing/pcoq.cmi \ + lib/pp.cmi lib/util.cmi parsing/g_zsyntax.cmi parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \ - parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx \ - lib/util.cmx parsing/g_zsyntax.cmi + parsing/esyntax.cmx parsing/extend.cmx kernel/names.cmx parsing/pcoq.cmx \ + lib/pp.cmx lib/util.cmx parsing/g_zsyntax.cmi parsing/lexer.cmo: parsing/lexer.cmi parsing/lexer.cmx: parsing/lexer.cmi -parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \ - lib/util.cmi parsing/pcoq.cmi -parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \ - lib/util.cmx parsing/pcoq.cmi +parsing/pcoq.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \ + parsing/lexer.cmi lib/options.cmi lib/pp.cmi proofs/tacexpr.cmo \ + lib/util.cmi toplevel/vernacexpr.cmo parsing/pcoq.cmi +parsing/pcoq.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/genarg.cmx \ + parsing/lexer.cmx lib/options.cmx lib/pp.cmx proofs/tacexpr.cmx \ + lib/util.cmx toplevel/vernacexpr.cmx parsing/pcoq.cmi +parsing/ppconstr.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \ + parsing/esyntax.cmi parsing/extend.cmi parsing/genarg.cmi \ + library/global.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi parsing/termast.cmi \ + lib/util.cmi parsing/ppconstr.cmi +parsing/ppconstr.cmx: parsing/ast.cmx parsing/coqast.cmx lib/dyn.cmx \ + parsing/esyntax.cmx parsing/extend.cmx parsing/genarg.cmx \ + library/global.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmx parsing/termast.cmx \ + lib/util.cmx parsing/ppconstr.cmi +parsing/pptactic.cmo: kernel/closure.cmi lib/dyn.cmi parsing/egrammar.cmi \ + parsing/extend.cmi parsing/genarg.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/ppconstr.cmi \ + parsing/printer.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo lib/util.cmi \ + parsing/pptactic.cmi +parsing/pptactic.cmx: kernel/closure.cmx lib/dyn.cmx parsing/egrammar.cmx \ + parsing/extend.cmx parsing/genarg.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/ppconstr.cmx \ + parsing/printer.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx lib/util.cmx \ + parsing/pptactic.cmi parsing/prettyp.cmo: pretyping/classops.cmi kernel/declarations.cmi \ library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \ library/global.cmi library/impargs.cmi kernel/inductive.cmi \ @@ -653,19 +742,25 @@ parsing/prettyp.cmx: pretyping/classops.cmx kernel/declarations.cmx \ kernel/safe_typing.cmx kernel/sign.cmx pretyping/syntax_def.cmx \ kernel/term.cmx pretyping/termops.cmx lib/util.cmx parsing/prettyp.cmi parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ - lib/dyn.cmi kernel/environ.cmi parsing/esyntax.cmi parsing/extend.cmi \ - library/global.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \ - kernel/sign.cmi kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \ - lib/util.cmi parsing/printer.cmi + kernel/environ.cmi parsing/extend.cmi library/global.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + pretyping/pattern.cmi lib/pp.cmi parsing/ppconstr.cmi kernel/sign.cmi \ + kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi lib/util.cmi \ + parsing/printer.cmi parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \ - lib/dyn.cmx kernel/environ.cmx parsing/esyntax.cmx parsing/extend.cmx \ - library/global.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \ - kernel/sign.cmx kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \ - lib/util.cmx parsing/printer.cmi -parsing/q_coqast.cmo: parsing/coqast.cmi kernel/names.cmi parsing/pcoq.cmi -parsing/q_coqast.cmx: parsing/coqast.cmx kernel/names.cmx parsing/pcoq.cmx + kernel/environ.cmx parsing/extend.cmx library/global.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + pretyping/pattern.cmx lib/pp.cmx parsing/ppconstr.cmx kernel/sign.cmx \ + kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx lib/util.cmx \ + parsing/printer.cmi +parsing/q_coqast.cmo: parsing/coqast.cmi parsing/genarg.cmi kernel/names.cmi \ + library/nametab.cmi parsing/pcoq.cmi parsing/q_util.cmi \ + pretyping/rawterm.cmi proofs/tacexpr.cmo +parsing/q_coqast.cmx: parsing/coqast.cmx parsing/genarg.cmx kernel/names.cmx \ + library/nametab.cmx parsing/pcoq.cmx parsing/q_util.cmx \ + pretyping/rawterm.cmx proofs/tacexpr.cmx +parsing/q_util.cmo: parsing/q_util.cmi +parsing/q_util.cmx: parsing/q_util.cmi parsing/search.cmo: parsing/astterm.cmi parsing/coqast.cmi parsing/coqlib.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ pretyping/evd.cmi library/global.cmi library/libobject.cmi \ @@ -682,6 +777,12 @@ parsing/search.cmx: parsing/astterm.cmx parsing/coqast.cmx parsing/coqlib.cmx \ pretyping/pretyping.cmx parsing/printer.cmx pretyping/rawterm.cmx \ pretyping/retyping.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ parsing/search.cmi +parsing/tacextend.cmo: parsing/ast.cmi parsing/genarg.cmi parsing/pcoq.cmi \ + lib/pp.cmi lib/pp_control.cmi parsing/q_coqast.cmo parsing/q_util.cmi \ + lib/util.cmi toplevel/vernacexpr.cmo +parsing/tacextend.cmx: parsing/ast.cmx parsing/genarg.cmx parsing/pcoq.cmx \ + lib/pp.cmx lib/pp_control.cmx parsing/q_coqast.cmx parsing/q_util.cmx \ + lib/util.cmx toplevel/vernacexpr.cmx parsing/termast.cmo: parsing/ast.cmi pretyping/classops.cmi \ parsing/coqast.cmi library/declare.cmi pretyping/detyping.cmi \ kernel/environ.cmi library/impargs.cmi kernel/inductive.cmi \ @@ -696,6 +797,12 @@ parsing/termast.cmx: parsing/ast.cmx pretyping/classops.cmx \ pretyping/pattern.cmx lib/pp.cmx pretyping/rawterm.cmx \ pretyping/reductionops.cmx kernel/sign.cmx kernel/term.cmx \ pretyping/termops.cmx kernel/univ.cmx lib/util.cmx parsing/termast.cmi +parsing/vernacextend.cmo: parsing/ast.cmi parsing/genarg.cmi parsing/pcoq.cmi \ + lib/pp.cmi lib/pp_control.cmi parsing/q_coqast.cmo parsing/q_util.cmi \ + lib/util.cmi toplevel/vernacexpr.cmo +parsing/vernacextend.cmx: parsing/ast.cmx parsing/genarg.cmx parsing/pcoq.cmx \ + lib/pp.cmx lib/pp_control.cmx parsing/q_coqast.cmx parsing/q_util.cmx \ + lib/util.cmx toplevel/vernacexpr.cmx pretyping/cases.cmo: pretyping/coercion.cmi kernel/declarations.cmi \ kernel/environ.cmi pretyping/evarconv.cmi pretyping/evarutil.cmi \ library/global.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ @@ -719,13 +826,13 @@ pretyping/cbv.cmx: kernel/closure.cmx kernel/environ.cmx kernel/esubst.cmx \ pretyping/evd.cmx pretyping/instantiate.cmx kernel/names.cmx lib/pp.cmx \ kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/cbv.cmi pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/global.cmi library/lib.cmi \ + pretyping/evd.cmi library/global.cmi library/goptions.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ library/nametab.cmi lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi \ pretyping/reductionops.cmi library/summary.cmi pretyping/tacred.cmi \ kernel/term.cmi pretyping/termops.cmi lib/util.cmi pretyping/classops.cmi pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \ - pretyping/evd.cmx library/global.cmx library/lib.cmx \ + pretyping/evd.cmx library/global.cmx library/goptions.cmx library/lib.cmx \ library/libobject.cmx library/library.cmx kernel/names.cmx \ library/nametab.cmx lib/options.cmx lib/pp.cmx pretyping/rawterm.cmx \ pretyping/reductionops.cmx library/summary.cmx pretyping/tacred.cmx \ @@ -900,16 +1007,16 @@ pretyping/tacred.cmo: pretyping/cbv.cmi kernel/closure.cmi \ kernel/conv_oracle.cmi kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \ pretyping/instantiate.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi pretyping/reductionops.cmi \ - library/summary.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ - pretyping/tacred.cmi + library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi \ + pretyping/reductionops.cmi pretyping/retyping.cmi library/summary.cmi \ + kernel/term.cmi pretyping/termops.cmi lib/util.cmi pretyping/tacred.cmi pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx \ kernel/conv_oracle.cmx kernel/declarations.cmx kernel/environ.cmx \ pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \ pretyping/instantiate.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/pp.cmx pretyping/reductionops.cmx \ - library/summary.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ - pretyping/tacred.cmi + library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmx \ + pretyping/reductionops.cmx pretyping/retyping.cmx library/summary.cmx \ + kernel/term.cmx pretyping/termops.cmx lib/util.cmx pretyping/tacred.cmi pretyping/termops.cmo: kernel/environ.cmi library/nameops.cmi \ kernel/names.cmi library/nametab.cmi lib/pp.cmi kernel/sign.cmi \ kernel/term.cmi kernel/univ.cmi lib/util.cmi pretyping/termops.cmi @@ -928,30 +1035,32 @@ proofs/clenv.cmo: kernel/environ.cmi proofs/evar_refiner.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi pretyping/instantiate.cmi \ proofs/logic.cmi library/nameops.cmi kernel/names.cmi lib/pp.cmi \ parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - pretyping/reductionops.cmi proofs/refiner.cmi pretyping/retyping.cmi \ - kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \ + pretyping/rawterm.cmi pretyping/reductionops.cmi proofs/refiner.cmi \ + pretyping/retyping.cmi kernel/sign.cmi proofs/tacexpr.cmo \ + proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \ pretyping/typing.cmi lib/util.cmi proofs/clenv.cmi proofs/clenv.cmx: kernel/environ.cmx proofs/evar_refiner.cmx \ pretyping/evarutil.cmx pretyping/evd.cmx pretyping/instantiate.cmx \ proofs/logic.cmx library/nameops.cmx kernel/names.cmx lib/pp.cmx \ parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - pretyping/reductionops.cmx proofs/refiner.cmx pretyping/retyping.cmx \ - kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \ + pretyping/rawterm.cmx pretyping/reductionops.cmx proofs/refiner.cmx \ + pretyping/retyping.cmx kernel/sign.cmx proofs/tacexpr.cmx \ + proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \ pretyping/typing.cmx lib/util.cmx proofs/clenv.cmi proofs/evar_refiner.cmo: parsing/astterm.cmi kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ pretyping/instantiate.cmi proofs/logic.cmi kernel/names.cmi \ lib/options.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ pretyping/reductionops.cmi proofs/refiner.cmi kernel/sign.cmi \ - pretyping/tacred.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ - proofs/evar_refiner.cmi + proofs/tacexpr.cmo pretyping/tacred.cmi kernel/term.cmi \ + pretyping/typing.cmi lib/util.cmi proofs/evar_refiner.cmi proofs/evar_refiner.cmx: parsing/astterm.cmx kernel/environ.cmx \ pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \ pretyping/instantiate.cmx proofs/logic.cmx kernel/names.cmx \ lib/options.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \ - pretyping/tacred.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ - proofs/evar_refiner.cmi + proofs/tacexpr.cmx pretyping/tacred.cmx kernel/term.cmx \ + pretyping/typing.cmx lib/util.cmx proofs/evar_refiner.cmi proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ kernel/inductive.cmi pretyping/inductiveops.cmi library/nameops.cmi \ @@ -971,229 +1080,257 @@ proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \ proofs/pfedit.cmo: parsing/astterm.cmi kernel/declarations.cmi \ library/declare.cmi lib/edit.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi library/lib.cmi \ - library/nameops.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi kernel/safe_typing.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ - proofs/pfedit.cmi + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + proofs/proof_trees.cmi proofs/proof_type.cmi kernel/safe_typing.cmi \ + kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi \ + lib/util.cmi proofs/pfedit.cmi proofs/pfedit.cmx: parsing/astterm.cmx kernel/declarations.cmx \ library/declare.cmx lib/edit.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx pretyping/evd.cmx library/lib.cmx \ - library/nameops.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx kernel/safe_typing.cmx kernel/sign.cmx \ - proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ - proofs/pfedit.cmi -proofs/proof_trees.cmo: parsing/ast.cmi kernel/closure.cmi \ - pretyping/detyping.cmi kernel/environ.cmi pretyping/evarutil.cmi \ - pretyping/evd.cmi library/global.cmi library/nameops.cmi kernel/names.cmi \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + proofs/proof_trees.cmx proofs/proof_type.cmx kernel/safe_typing.cmx \ + kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx \ + lib/util.cmx proofs/pfedit.cmi +proofs/proof_trees.cmo: kernel/closure.cmi pretyping/detyping.cmi \ + kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ + library/global.cmi library/nameops.cmi kernel/names.cmi \ library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \ - kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi parsing/termast.cmi \ + kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi \ pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ proofs/proof_trees.cmi -proofs/proof_trees.cmx: parsing/ast.cmx kernel/closure.cmx \ - pretyping/detyping.cmx kernel/environ.cmx pretyping/evarutil.cmx \ - pretyping/evd.cmx library/global.cmx library/nameops.cmx kernel/names.cmx \ +proofs/proof_trees.cmx: kernel/closure.cmx pretyping/detyping.cmx \ + kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ + library/global.cmx library/nameops.cmx kernel/names.cmx \ library/nametab.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \ - kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx parsing/termast.cmx \ + kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx \ pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ proofs/proof_trees.cmi -proofs/proof_type.cmo: parsing/coqast.cmi kernel/environ.cmi \ - pretyping/evd.cmi kernel/names.cmi library/nametab.cmi \ - pretyping/pretyping.cmi pretyping/tacred.cmi kernel/term.cmi lib/util.cmi \ +proofs/proof_type.cmo: kernel/closure.cmi kernel/environ.cmi \ + pretyping/evd.cmi parsing/genarg.cmi kernel/names.cmi library/nametab.cmi \ + pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi lib/util.cmi \ proofs/proof_type.cmi -proofs/proof_type.cmx: parsing/coqast.cmx kernel/environ.cmx \ - pretyping/evd.cmx kernel/names.cmx library/nametab.cmx \ - pretyping/pretyping.cmx pretyping/tacred.cmx kernel/term.cmx lib/util.cmx \ +proofs/proof_type.cmx: kernel/closure.cmx kernel/environ.cmx \ + pretyping/evd.cmx parsing/genarg.cmx kernel/names.cmx library/nametab.cmx \ + pretyping/rawterm.cmx proofs/tacexpr.cmx kernel/term.cmx lib/util.cmx \ proofs/proof_type.cmi -proofs/refiner.cmo: parsing/ast.cmi kernel/environ.cmi pretyping/evarutil.cmi \ +proofs/refiner.cmo: kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/global.cmi pretyping/instantiate.cmi \ - proofs/logic.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi pretyping/reductionops.cmi kernel/sign.cmi \ - kernel/term.cmi pretyping/termops.cmi kernel/type_errors.cmi lib/util.cmi \ - proofs/refiner.cmi -proofs/refiner.cmx: parsing/ast.cmx kernel/environ.cmx pretyping/evarutil.cmx \ + proofs/logic.cmi lib/pp.cmi parsing/pptactic.cmi parsing/printer.cmi \ + proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \ + kernel/sign.cmi proofs/tacexpr.cmo kernel/term.cmi pretyping/termops.cmi \ + kernel/type_errors.cmi lib/util.cmi proofs/refiner.cmi +proofs/refiner.cmx: kernel/environ.cmx pretyping/evarutil.cmx \ pretyping/evd.cmx library/global.cmx pretyping/instantiate.cmx \ - proofs/logic.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx pretyping/reductionops.cmx kernel/sign.cmx \ - kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \ - proofs/refiner.cmi -proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \ - kernel/conv_oracle.cmi parsing/coqast.cmi kernel/declarations.cmi \ - library/declare.cmi lib/dyn.cmi kernel/environ.cmi pretyping/evd.cmi \ - library/global.cmi lib/gmap.cmi library/lib.cmi library/libobject.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ - pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi \ - pretyping/pretyping.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ - pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/sign.cmi \ - library/summary.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ - proofs/tactic_debug.cmi kernel/term.cmi pretyping/termops.cmi \ - pretyping/typing.cmi lib/util.cmi proofs/tacinterp.cmi -proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \ - kernel/conv_oracle.cmx parsing/coqast.cmx kernel/declarations.cmx \ - library/declare.cmx lib/dyn.cmx kernel/environ.cmx pretyping/evd.cmx \ - library/global.cmx lib/gmap.cmx library/lib.cmx library/libobject.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ - pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx \ - pretyping/pretyping.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ - pretyping/reductionops.cmx kernel/safe_typing.cmx kernel/sign.cmx \ - library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ - proofs/tactic_debug.cmx kernel/term.cmx pretyping/termops.cmx \ - pretyping/typing.cmx lib/util.cmx proofs/tacinterp.cmi + proofs/logic.cmx lib/pp.cmx parsing/pptactic.cmx parsing/printer.cmx \ + proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \ + kernel/sign.cmx proofs/tacexpr.cmx kernel/term.cmx pretyping/termops.cmx \ + kernel/type_errors.cmx lib/util.cmx proofs/refiner.cmi +proofs/tacexpr.cmo: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \ + kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi lib/util.cmi +proofs/tacexpr.cmx: parsing/coqast.cmx lib/dyn.cmx parsing/genarg.cmx \ + kernel/names.cmx library/nametab.cmx pretyping/rawterm.cmx lib/util.cmx proofs/tacmach.cmo: parsing/astterm.cmi library/declare.cmi \ kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ library/global.cmi pretyping/instantiate.cmi proofs/logic.cmi \ library/nameops.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \ - proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi \ + proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ + pretyping/reductionops.cmi proofs/refiner.cmi kernel/sign.cmi \ + proofs/tacexpr.cmo pretyping/tacred.cmi kernel/term.cmi \ pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ proofs/tacmach.cmi proofs/tacmach.cmx: parsing/astterm.cmx library/declare.cmx \ kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ library/global.cmx pretyping/instantiate.cmx proofs/logic.cmx \ library/nameops.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \ - proofs/refiner.cmx kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx \ + proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ + pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \ + proofs/tacexpr.cmx pretyping/tacred.cmx kernel/term.cmx \ pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ proofs/tacmach.cmi -proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi proofs/tacmach.cmi proofs/tactic_debug.cmi -proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx proofs/tacmach.cmx proofs/tactic_debug.cmi +proofs/tactic_debug.cmo: parsing/ast.cmi kernel/names.cmi lib/pp.cmi \ + parsing/pptactic.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + proofs/tacmach.cmi proofs/tactic_debug.cmi +proofs/tactic_debug.cmx: parsing/ast.cmx kernel/names.cmx lib/pp.cmx \ + parsing/pptactic.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + proofs/tacmach.cmx proofs/tactic_debug.cmi scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \ - parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ - tactics/dhyp.cmi proofs/evar_refiner.cmi pretyping/evd.cmi \ - library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \ - kernel/inductive.cmi library/lib.cmi library/libobject.cmi \ - library/library.cmi proofs/logic.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi pretyping/pattern.cmi \ - proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \ - pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \ - library/summary.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi tactics/auto.cmi + kernel/declarations.cmi library/declare.cmi tactics/dhyp.cmi \ + proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \ + tactics/hiddentac.cmi tactics/hipattern.cmi kernel/inductive.cmi \ + library/lib.cmi library/libobject.cmi library/library.cmi \ + proofs/logic.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \ + lib/options.cmi pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi \ + parsing/pptactic.cmi parsing/printer.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \ + kernel/sign.cmi library/summary.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ + pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo tactics/auto.cmi tactics/auto.cmx: parsing/astterm.cmx tactics/btermdn.cmx proofs/clenv.cmx \ - parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \ - tactics/dhyp.cmx proofs/evar_refiner.cmx pretyping/evd.cmx \ - library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \ - kernel/inductive.cmx library/lib.cmx library/libobject.cmx \ - library/library.cmx proofs/logic.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx pretyping/pattern.cmx \ - proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \ - pretyping/rawterm.cmx kernel/reduction.cmx kernel/sign.cmx \ - library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx tactics/auto.cmi -tactics/autorewrite.cmo: parsing/ast.cmi toplevel/command.cmi \ - parsing/coqast.cmi tactics/equality.cmi tactics/hipattern.cmi \ - library/lib.cmi library/libobject.cmi kernel/names.cmi lib/pp.cmi \ - proofs/proof_type.cmi library/summary.cmi proofs/tacinterp.cmi \ - proofs/tacmach.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \ - kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - tactics/autorewrite.cmi -tactics/autorewrite.cmx: parsing/ast.cmx toplevel/command.cmx \ - parsing/coqast.cmx tactics/equality.cmx tactics/hipattern.cmx \ - library/lib.cmx library/libobject.cmx kernel/names.cmx lib/pp.cmx \ - proofs/proof_type.cmx library/summary.cmx proofs/tacinterp.cmx \ - proofs/tacmach.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \ - kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - tactics/autorewrite.cmi + kernel/declarations.cmx library/declare.cmx tactics/dhyp.cmx \ + proofs/evar_refiner.cmx pretyping/evd.cmx library/global.cmx \ + tactics/hiddentac.cmx tactics/hipattern.cmx kernel/inductive.cmx \ + library/lib.cmx library/libobject.cmx library/library.cmx \ + proofs/logic.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \ + lib/options.cmx pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx \ + parsing/pptactic.cmx parsing/printer.cmx proofs/proof_type.cmx \ + pretyping/rawterm.cmx kernel/reduction.cmx proofs/refiner.cmx \ + kernel/sign.cmx library/summary.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ + pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx tactics/auto.cmi +tactics/autorewrite.cmo: parsing/ast.cmi parsing/coqast.cmi \ + tactics/equality.cmi tactics/hipattern.cmi library/lib.cmi \ + library/libobject.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ + library/summary.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi tactics/autorewrite.cmi +tactics/autorewrite.cmx: parsing/ast.cmx parsing/coqast.cmx \ + tactics/equality.cmx tactics/hipattern.cmx library/lib.cmx \ + library/libobject.cmx kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx \ + library/summary.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx tactics/autorewrite.cmi tactics/btermdn.cmo: tactics/dn.cmi pretyping/pattern.cmi kernel/term.cmi \ tactics/termdn.cmi tactics/btermdn.cmi tactics/btermdn.cmx: tactics/dn.cmx pretyping/pattern.cmx kernel/term.cmx \ tactics/termdn.cmx tactics/btermdn.cmi +tactics/contradiction.cmo: parsing/coqlib.cmi tactics/hipattern.cmi \ + proofs/proof_type.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi lib/util.cmi \ + tactics/contradiction.cmi +tactics/contradiction.cmx: parsing/coqlib.cmx tactics/hipattern.cmx \ + proofs/proof_type.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx lib/util.cmx \ + tactics/contradiction.cmi tactics/dhyp.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \ parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \ library/global.cmi library/lib.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi tactics/nbtermdn.cmi \ pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi proofs/proof_type.cmi \ - pretyping/rawterm.cmi kernel/reduction.cmi library/summary.cmi \ - proofs/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi tactics/dhyp.cmi + pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \ + library/summary.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \ + tactics/dhyp.cmi tactics/dhyp.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \ parsing/coqast.cmx kernel/environ.cmx pretyping/evd.cmx \ library/global.cmx library/lib.cmx library/libobject.cmx \ library/library.cmx kernel/names.cmx tactics/nbtermdn.cmx \ pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx proofs/proof_type.cmx \ - pretyping/rawterm.cmx kernel/reduction.cmx library/summary.cmx \ - proofs/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx tactics/dhyp.cmi + pretyping/rawterm.cmx kernel/reduction.cmx proofs/refiner.cmx \ + library/summary.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \ + tactics/dhyp.cmi tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi -tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi proofs/evar_refiner.cmi \ - lib/explore.cmi proofs/logic.cmi library/nameops.cmi kernel/names.cmi \ - pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \ - proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - kernel/term.cmi pretyping/termops.cmi lib/util.cmi -tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx proofs/evar_refiner.cmx \ - lib/explore.cmx proofs/logic.cmx library/nameops.cmx kernel/names.cmx \ - pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \ - proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - kernel/term.cmx pretyping/termops.cmx lib/util.cmx -tactics/elim.cmo: proofs/clenv.cmi library/declare.cmi kernel/environ.cmi \ - tactics/hiddentac.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi \ - kernel/reduction.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ +tactics/eauto.cmo: tactics/auto.cmi toplevel/cerrors.cmi proofs/clenv.cmi \ + parsing/egrammar.cmi proofs/evar_refiner.cmi lib/explore.cmi \ + parsing/genarg.cmi proofs/logic.cmi library/nameops.cmi kernel/names.cmi \ + pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \ + proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ + kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi \ + tactics/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi +tactics/eauto.cmx: tactics/auto.cmx toplevel/cerrors.cmx proofs/clenv.cmx \ + parsing/egrammar.cmx proofs/evar_refiner.cmx lib/explore.cmx \ + parsing/genarg.cmx proofs/logic.cmx library/nameops.cmx kernel/names.cmx \ + pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \ + proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ + kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx \ + tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx +tactics/elim.cmo: proofs/clenv.cmi kernel/environ.cmi tactics/hiddentac.cmi \ + tactics/hipattern.cmi pretyping/inductiveops.cmi kernel/names.cmi \ + library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \ + proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \ tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ tactics/elim.cmi -tactics/elim.cmx: proofs/clenv.cmx library/declare.cmx kernel/environ.cmx \ - tactics/hiddentac.cmx tactics/hipattern.cmx pretyping/inductiveops.cmx \ - kernel/names.cmx library/nametab.cmx lib/pp.cmx proofs/proof_type.cmx \ - kernel/reduction.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ +tactics/elim.cmx: proofs/clenv.cmx kernel/environ.cmx tactics/hiddentac.cmx \ + tactics/hipattern.cmx pretyping/inductiveops.cmx kernel/names.cmx \ + library/nametab.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \ + pretyping/rawterm.cmx kernel/reduction.cmx proofs/refiner.cmx \ + proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ tactics/elim.cmi -tactics/eqdecide.cmo: tactics/auto.cmi parsing/coqlib.cmi \ - kernel/declarations.cmi tactics/equality.cmi library/global.cmi \ - tactics/hiddentac.cmi tactics/hipattern.cmi library/nameops.cmi \ - kernel/names.cmi pretyping/pattern.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi lib/util.cmi -tactics/eqdecide.cmx: tactics/auto.cmx parsing/coqlib.cmx \ - kernel/declarations.cmx tactics/equality.cmx library/global.cmx \ - tactics/hiddentac.cmx tactics/hipattern.cmx library/nameops.cmx \ - kernel/names.cmx pretyping/pattern.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx lib/util.cmx -tactics/equality.cmo: parsing/astterm.cmi proofs/clenv.cmi parsing/coqast.cmi \ - parsing/coqlib.cmi kernel/declarations.cmi kernel/environ.cmi \ - proofs/evar_refiner.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ - library/global.cmi lib/gmapl.cmi tactics/hipattern.cmi \ +tactics/eqdecide.cmo: tactics/auto.cmi toplevel/cerrors.cmi \ + parsing/coqlib.cmi kernel/declarations.cmi parsing/egrammar.cmi \ + tactics/equality.cmi tactics/extratactics.cmi parsing/genarg.cmi \ + library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \ + library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi \ + parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi proofs/refiner.cmi proofs/tacmach.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi +tactics/eqdecide.cmx: tactics/auto.cmx toplevel/cerrors.cmx \ + parsing/coqlib.cmx kernel/declarations.cmx parsing/egrammar.cmx \ + tactics/equality.cmx tactics/extratactics.cmx parsing/genarg.cmx \ + library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \ + library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx \ + parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx proofs/refiner.cmx proofs/tacmach.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx +tactics/equality.cmo: proofs/clenv.cmi parsing/coqast.cmi parsing/coqlib.cmi \ + kernel/declarations.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ + pretyping/evarutil.cmi lib/gmapl.cmi tactics/hipattern.cmi \ pretyping/indrec.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ - pretyping/instantiate.cmi library/lib.cmi library/libobject.cmi \ - proofs/logic.cmi library/nameops.cmi kernel/names.cmi \ - pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ - pretyping/reductionops.cmi pretyping/retyping.cmi \ - tactics/setoid_replace.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ - pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi \ - pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi tactics/wcclausenv.cmi tactics/equality.cmi -tactics/equality.cmx: parsing/astterm.cmx proofs/clenv.cmx parsing/coqast.cmx \ - parsing/coqlib.cmx kernel/declarations.cmx kernel/environ.cmx \ - proofs/evar_refiner.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ - library/global.cmx lib/gmapl.cmx tactics/hipattern.cmx \ + pretyping/instantiate.cmi library/libobject.cmi proofs/logic.cmi \ + library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \ + pretyping/retyping.cmi tactics/setoid_replace.cmi tactics/tacinterp.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \ + kernel/typeops.cmi pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi tactics/wcclausenv.cmi \ + tactics/equality.cmi +tactics/equality.cmx: proofs/clenv.cmx parsing/coqast.cmx parsing/coqlib.cmx \ + kernel/declarations.cmx kernel/environ.cmx proofs/evar_refiner.cmx \ + pretyping/evarutil.cmx lib/gmapl.cmx tactics/hipattern.cmx \ pretyping/indrec.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ - pretyping/instantiate.cmx library/lib.cmx library/libobject.cmx \ - proofs/logic.cmx library/nameops.cmx kernel/names.cmx \ - pretyping/pattern.cmx lib/pp.cmx proofs/proof_type.cmx \ - pretyping/reductionops.cmx pretyping/retyping.cmx \ - tactics/setoid_replace.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ - pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \ - pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx tactics/wcclausenv.cmx tactics/equality.cmi -tactics/hiddentac.cmo: proofs/proof_type.cmi tactics/tacentries.cmi \ - proofs/tacmach.cmi kernel/term.cmi tactics/hiddentac.cmi -tactics/hiddentac.cmx: proofs/proof_type.cmx tactics/tacentries.cmx \ - proofs/tacmach.cmx kernel/term.cmx tactics/hiddentac.cmi + pretyping/instantiate.cmx library/libobject.cmx proofs/logic.cmx \ + library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ + proofs/proof_type.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \ + pretyping/retyping.cmx tactics/setoid_replace.cmx tactics/tacinterp.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \ + kernel/typeops.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx tactics/wcclausenv.cmx \ + tactics/equality.cmi +tactics/extraargs.cmo: parsing/genarg.cmi toplevel/metasyntax.cmi \ + parsing/pcoq.cmi lib/pp.cmi parsing/ppconstr.cmi parsing/pptactic.cmi \ + parsing/printer.cmi tactics/tacinterp.cmi tactics/extraargs.cmi +tactics/extraargs.cmx: parsing/genarg.cmx toplevel/metasyntax.cmx \ + parsing/pcoq.cmx lib/pp.cmx parsing/ppconstr.cmx parsing/pptactic.cmx \ + parsing/printer.cmx tactics/tacinterp.cmx tactics/extraargs.cmi +tactics/extratactics.cmo: parsing/astterm.cmi tactics/autorewrite.cmi \ + toplevel/cerrors.cmi tactics/contradiction.cmi parsing/coqast.cmi \ + parsing/egrammar.cmi tactics/equality.cmi pretyping/evd.cmi \ + tactics/extraargs.cmi parsing/genarg.cmi library/global.cmi \ + tactics/inv.cmi tactics/leminv.cmi parsing/pcoq.cmi lib/pp.cmi \ + parsing/pptactic.cmi pretyping/rawterm.cmi tactics/refine.cmi \ + proofs/refiner.cmi tactics/setoid_replace.cmi proofs/tacexpr.cmo \ + tactics/tacinterp.cmi kernel/term.cmi toplevel/vernacinterp.cmi \ + tactics/extratactics.cmi +tactics/extratactics.cmx: parsing/astterm.cmx tactics/autorewrite.cmx \ + toplevel/cerrors.cmx tactics/contradiction.cmx parsing/coqast.cmx \ + parsing/egrammar.cmx tactics/equality.cmx pretyping/evd.cmx \ + tactics/extraargs.cmx parsing/genarg.cmx library/global.cmx \ + tactics/inv.cmx tactics/leminv.cmx parsing/pcoq.cmx lib/pp.cmx \ + parsing/pptactic.cmx pretyping/rawterm.cmx tactics/refine.cmx \ + proofs/refiner.cmx tactics/setoid_replace.cmx proofs/tacexpr.cmx \ + tactics/tacinterp.cmx kernel/term.cmx toplevel/vernacinterp.cmx \ + tactics/extratactics.cmi +tactics/hiddentac.cmo: proofs/evar_refiner.cmi kernel/names.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi proofs/refiner.cmi \ + proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tactics.cmi kernel/term.cmi \ + lib/util.cmi tactics/hiddentac.cmi +tactics/hiddentac.cmx: proofs/evar_refiner.cmx kernel/names.cmx \ + proofs/proof_type.cmx pretyping/rawterm.cmx proofs/refiner.cmx \ + proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tactics.cmx kernel/term.cmx \ + lib/util.cmx tactics/hiddentac.cmi tactics/hipattern.cmo: proofs/clenv.cmi parsing/coqlib.cmi \ kernel/declarations.cmi kernel/environ.cmi pretyping/evd.cmi \ library/global.cmi pretyping/inductiveops.cmi library/nameops.cmi \ @@ -1210,100 +1347,122 @@ tactics/inv.cmo: proofs/clenv.cmi parsing/coqlib.cmi tactics/elim.cmi \ kernel/environ.cmi tactics/equality.cmi proofs/evar_refiner.cmi \ library/global.cmi pretyping/inductiveops.cmi library/nameops.cmi \ kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_type.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ - pretyping/retyping.cmi kernel/sign.cmi proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ - tactics/wcclausenv.cmi tactics/inv.cmi + proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ + pretyping/reductionops.cmi pretyping/retyping.cmi kernel/sign.cmi \ + proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \ + pretyping/typing.cmi lib/util.cmi tactics/wcclausenv.cmi tactics/inv.cmi tactics/inv.cmx: proofs/clenv.cmx parsing/coqlib.cmx tactics/elim.cmx \ kernel/environ.cmx tactics/equality.cmx proofs/evar_refiner.cmx \ library/global.cmx pretyping/inductiveops.cmx library/nameops.cmx \ kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_type.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ - pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ - tactics/wcclausenv.cmx tactics/inv.cmi + proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ + pretyping/reductionops.cmx pretyping/retyping.cmx kernel/sign.cmx \ + proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \ + pretyping/typing.cmx lib/util.cmx tactics/wcclausenv.cmx tactics/inv.cmi tactics/leminv.cmo: parsing/astterm.cmi proofs/clenv.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \ pretyping/inductiveops.cmi tactics/inv.cmi library/nameops.cmi \ - kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \ - kernel/safe_typing.cmi kernel/sign.cmi proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - tactics/wcclausenv.cmi + kernel/names.cmi library/nametab.cmi proofs/pfedit.cmi lib/pp.cmi \ + parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/sign.cmi \ + proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo tactics/wcclausenv.cmi tactics/leminv.cmi tactics/leminv.cmx: parsing/astterm.cmx proofs/clenv.cmx \ kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx pretyping/evd.cmx library/global.cmx \ pretyping/inductiveops.cmx tactics/inv.cmx library/nameops.cmx \ - kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \ - kernel/safe_typing.cmx kernel/sign.cmx proofs/tacmach.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - tactics/wcclausenv.cmx + kernel/names.cmx library/nametab.cmx proofs/pfedit.cmx lib/pp.cmx \ + parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + pretyping/reductionops.cmx kernel/safe_typing.cmx kernel/sign.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx tactics/wcclausenv.cmx tactics/leminv.cmi tactics/nbtermdn.cmo: tactics/btermdn.cmi lib/gmap.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi pretyping/pattern.cmi \ kernel/term.cmi tactics/termdn.cmi lib/util.cmi tactics/nbtermdn.cmi tactics/nbtermdn.cmx: tactics/btermdn.cmx lib/gmap.cmx library/libobject.cmx \ library/library.cmx kernel/names.cmx pretyping/pattern.cmx \ kernel/term.cmx tactics/termdn.cmx lib/util.cmx tactics/nbtermdn.cmi -tactics/refine.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/environ.cmi \ - pretyping/evd.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_type.cmi kernel/reduction.cmi pretyping/retyping.cmi \ - kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \ - pretyping/typing.cmi lib/util.cmi tactics/refine.cmi -tactics/refine.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/environ.cmx \ - pretyping/evd.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_type.cmx kernel/reduction.cmx pretyping/retyping.cmx \ - kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \ - pretyping/typing.cmx lib/util.cmx tactics/refine.cmi +tactics/refine.cmo: proofs/clenv.cmi kernel/environ.cmi pretyping/evd.cmi \ + kernel/names.cmi lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi \ + pretyping/retyping.cmi kernel/sign.cmi proofs/tacmach.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ + pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ + tactics/refine.cmi +tactics/refine.cmx: proofs/clenv.cmx kernel/environ.cmx pretyping/evd.cmx \ + kernel/names.cmx lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx \ + pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ + pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ + tactics/refine.cmi tactics/setoid_replace.cmo: parsing/astterm.cmi tactics/auto.cmi \ toplevel/command.cmi library/declare.cmi kernel/environ.cmi \ pretyping/evd.cmi library/global.cmi lib/gmap.cmi library/lib.cmi \ library/libobject.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \ - kernel/safe_typing.cmi library/summary.cmi proofs/tacmach.cmi \ + library/nametab.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_type.cmi pretyping/reductionops.cmi kernel/safe_typing.cmi \ + library/summary.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi \ pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ - toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \ - tactics/setoid_replace.cmi + toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacinterp.cmi tactics/setoid_replace.cmi tactics/setoid_replace.cmx: parsing/astterm.cmx tactics/auto.cmx \ toplevel/command.cmx library/declare.cmx kernel/environ.cmx \ pretyping/evd.cmx library/global.cmx lib/gmap.cmx library/lib.cmx \ library/libobject.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \ - kernel/safe_typing.cmx library/summary.cmx proofs/tacmach.cmx \ + library/nametab.cmx lib/options.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_type.cmx pretyping/reductionops.cmx kernel/safe_typing.cmx \ + library/summary.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \ pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ - toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \ - tactics/setoid_replace.cmi -tactics/tacentries.cmo: proofs/evar_refiner.cmi proofs/proof_trees.cmi \ - proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - tactics/tacentries.cmi -tactics/tacentries.cmx: proofs/evar_refiner.cmx proofs/proof_trees.cmx \ - proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - tactics/tacentries.cmi -tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \ - kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ - proofs/evar_refiner.cmi library/global.cmi pretyping/indrec.cmi \ - kernel/inductive.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ - kernel/reduction.cmi kernel/sign.cmi proofs/tacinterp.cmi \ - proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \ + toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacinterp.cmx tactics/setoid_replace.cmi +tactics/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi tactics/auto.cmi \ + kernel/closure.cmi parsing/coqast.cmi kernel/declarations.cmi \ + library/declare.cmi tactics/dhyp.cmi lib/dyn.cmi tactics/elim.cmi \ + kernel/environ.cmi pretyping/evd.cmi parsing/genarg.cmi \ + library/global.cmi lib/gmap.cmi tactics/hiddentac.cmi library/lib.cmi \ + library/libobject.cmi proofs/logic.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/options.cmi \ + pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi \ + pretyping/pretype_errors.cmi pretyping/pretyping.cmi parsing/printer.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \ + proofs/refiner.cmi kernel/safe_typing.cmi kernel/sign.cmi \ + library/summary.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ + pretyping/tacred.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \ + kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \ + pretyping/typing.cmi lib/util.cmi tactics/tacinterp.cmi +tactics/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx tactics/auto.cmx \ + kernel/closure.cmx parsing/coqast.cmx kernel/declarations.cmx \ + library/declare.cmx tactics/dhyp.cmx lib/dyn.cmx tactics/elim.cmx \ + kernel/environ.cmx pretyping/evd.cmx parsing/genarg.cmx \ + library/global.cmx lib/gmap.cmx tactics/hiddentac.cmx library/lib.cmx \ + library/libobject.cmx proofs/logic.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/options.cmx \ + pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx \ + pretyping/pretype_errors.cmx pretyping/pretyping.cmx parsing/printer.cmx \ + proofs/proof_type.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \ + proofs/refiner.cmx kernel/safe_typing.cmx kernel/sign.cmx \ + library/summary.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ + pretyping/tacred.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \ + kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \ + pretyping/typing.cmx lib/util.cmx tactics/tacinterp.cmi +tactics/tacticals.cmo: proofs/clenv.cmi kernel/declarations.cmi \ + library/declare.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ + library/global.cmi pretyping/indrec.cmi kernel/inductive.cmi \ + kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi kernel/reduction.cmi \ + proofs/refiner.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ pretyping/termops.cmi lib/util.cmi tactics/wcclausenv.cmi \ tactics/tacticals.cmi -tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \ - kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ - proofs/evar_refiner.cmx library/global.cmx pretyping/indrec.cmx \ - kernel/inductive.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ - kernel/reduction.cmx kernel/sign.cmx proofs/tacinterp.cmx \ - proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \ +tactics/tacticals.cmx: proofs/clenv.cmx kernel/declarations.cmx \ + library/declare.cmx kernel/environ.cmx proofs/evar_refiner.cmx \ + library/global.cmx pretyping/indrec.cmx kernel/inductive.cmx \ + kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx kernel/reduction.cmx \ + proofs/refiner.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \ pretyping/termops.cmx lib/util.cmx tactics/wcclausenv.cmx \ tactics/tacticals.cmi tactics/tactics.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/closure.cmi \ @@ -1313,10 +1472,10 @@ tactics/tactics.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/closure.cmi \ kernel/inductive.cmi pretyping/inductiveops.cmi proofs/logic.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi \ proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - pretyping/reductionops.cmi proofs/refiner.cmi kernel/safe_typing.cmi \ - kernel/sign.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ - pretyping/tacred.cmi tactics/tacticals.cmi kernel/term.cmi \ - pretyping/termops.cmi lib/util.cmi tactics/tactics.cmi + pretyping/rawterm.cmi pretyping/reductionops.cmi proofs/refiner.cmi \ + kernel/safe_typing.cmi kernel/sign.cmi proofs/tacexpr.cmo \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ + kernel/term.cmi pretyping/termops.cmi lib/util.cmi tactics/tactics.cmi tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \ parsing/coqlib.cmx kernel/declarations.cmx library/declare.cmx \ kernel/environ.cmx proofs/evar_refiner.cmx pretyping/evd.cmx \ @@ -1324,16 +1483,22 @@ tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \ kernel/inductive.cmx pretyping/inductiveops.cmx proofs/logic.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx \ proofs/pfedit.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - pretyping/reductionops.cmx proofs/refiner.cmx kernel/safe_typing.cmx \ - kernel/sign.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ - pretyping/tacred.cmx tactics/tacticals.cmx kernel/term.cmx \ - pretyping/termops.cmx lib/util.cmx tactics/tactics.cmi -tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \ - kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \ - proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi lib/util.cmi -tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \ - kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \ - proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx lib/util.cmx + pretyping/rawterm.cmx pretyping/reductionops.cmx proofs/refiner.cmx \ + kernel/safe_typing.cmx kernel/sign.cmx proofs/tacexpr.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ + kernel/term.cmx pretyping/termops.cmx lib/util.cmx tactics/tactics.cmi +tactics/tauto.cmo: parsing/ast.cmi toplevel/cerrors.cmi parsing/coqast.cmi \ + parsing/egrammar.cmi parsing/genarg.cmi tactics/hipattern.cmi \ + kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi \ + parsing/pptactic.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ + proofs/refiner.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi lib/util.cmi +tactics/tauto.cmx: parsing/ast.cmx toplevel/cerrors.cmx parsing/coqast.cmx \ + parsing/egrammar.cmx parsing/genarg.cmx tactics/hipattern.cmx \ + kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx \ + parsing/pptactic.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ + proofs/refiner.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx lib/util.cmx tactics/termdn.cmo: tactics/dn.cmi library/nameops.cmi kernel/names.cmi \ library/nametab.cmi pretyping/pattern.cmi pretyping/rawterm.cmi \ kernel/term.cmi lib/util.cmi tactics/termdn.cmi @@ -1343,15 +1508,15 @@ tactics/termdn.cmx: tactics/dn.cmx library/nameops.cmx kernel/names.cmx \ tactics/wcclausenv.cmo: proofs/clenv.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \ proofs/logic.cmi library/nameops.cmi kernel/names.cmi lib/pp.cmi \ - proofs/proof_trees.cmi pretyping/reductionops.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ - tactics/wcclausenv.cmi + proofs/proof_trees.cmi pretyping/reductionops.cmi proofs/refiner.cmi \ + kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \ + lib/util.cmi tactics/wcclausenv.cmi tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx pretyping/evd.cmx library/global.cmx \ proofs/logic.cmx library/nameops.cmx kernel/names.cmx lib/pp.cmx \ - proofs/proof_trees.cmx pretyping/reductionops.cmx kernel/sign.cmx \ - proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ - tactics/wcclausenv.cmi + proofs/proof_trees.cmx pretyping/reductionops.cmx proofs/refiner.cmx \ + kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \ + lib/util.cmx tactics/wcclausenv.cmi tools/coqdep_lexer.cmo: config/coq_config.cmi tools/coqdep_lexer.cmx: config/coq_config.cmx tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo @@ -1363,48 +1528,50 @@ tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \ kernel/indtypes.cmi parsing/lexer.cmi proofs/logic.cmi \ library/nametab.cmi lib/options.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi proofs/tacmach.cmi kernel/type_errors.cmi \ + pretyping/pretype_errors.cmi proofs/refiner.cmi kernel/type_errors.cmi \ kernel/univ.cmi lib/util.cmi toplevel/cerrors.cmi toplevel/cerrors.cmx: parsing/ast.cmx pretyping/cases.cmx toplevel/himsg.cmx \ kernel/indtypes.cmx parsing/lexer.cmx proofs/logic.cmx \ library/nametab.cmx lib/options.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx proofs/tacmach.cmx kernel/type_errors.cmx \ + pretyping/pretype_errors.cmx proofs/refiner.cmx kernel/type_errors.cmx \ kernel/univ.cmx lib/util.cmx toplevel/cerrors.cmi toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \ library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \ library/global.cmi kernel/inductive.cmi library/lib.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ - parsing/printer.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ - kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \ - pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + lib/pp.cmi parsing/printer.cmi pretyping/reductionops.cmi \ + pretyping/retyping.cmi kernel/safe_typing.cmi kernel/sign.cmi \ + kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ toplevel/class.cmi toplevel/class.cmx: pretyping/classops.cmx kernel/declarations.cmx \ library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \ library/global.cmx kernel/inductive.cmx library/lib.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ - parsing/printer.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ - kernel/safe_typing.cmx kernel/sign.cmx kernel/term.cmx \ - pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + lib/pp.cmx parsing/printer.cmx pretyping/reductionops.cmx \ + pretyping/retyping.cmx kernel/safe_typing.cmx kernel/sign.cmx \ + kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/class.cmi -toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \ - kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/global.cmi library/impargs.cmi \ - pretyping/indrec.cmi kernel/indtypes.cmi kernel/inductive.cmi \ - library/lib.cmi library/libobject.cmi library/library.cmi \ - proofs/logic.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \ - lib/options.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_type.cmi kernel/reduction.cmi kernel/safe_typing.cmi \ +toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \ + parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ + kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ + tactics/hiddentac.cmi library/impargs.cmi pretyping/indrec.cmi \ + kernel/indtypes.cmi kernel/inductive.cmi library/lib.cmi \ + library/libobject.cmi library/library.cmi proofs/logic.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \ + kernel/reduction.cmi proofs/refiner.cmi kernel/safe_typing.cmi \ library/states.cmi pretyping/syntax_def.cmi proofs/tacmach.cmi \ pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi \ kernel/typeops.cmi lib/util.cmi toplevel/command.cmi -toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \ - kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ - pretyping/evd.cmx library/global.cmx library/impargs.cmx \ - pretyping/indrec.cmx kernel/indtypes.cmx kernel/inductive.cmx \ - library/lib.cmx library/libobject.cmx library/library.cmx \ - proofs/logic.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \ - lib/options.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_type.cmx kernel/reduction.cmx kernel/safe_typing.cmx \ +toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \ + parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \ + kernel/environ.cmx pretyping/evd.cmx library/global.cmx \ + tactics/hiddentac.cmx library/impargs.cmx pretyping/indrec.cmx \ + kernel/indtypes.cmx kernel/inductive.cmx library/lib.cmx \ + library/libobject.cmx library/library.cmx proofs/logic.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \ + kernel/reduction.cmx proofs/refiner.cmx kernel/safe_typing.cmx \ library/states.cmx pretyping/syntax_def.cmx proofs/tacmach.cmx \ pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx \ kernel/typeops.cmx lib/util.cmx toplevel/command.cmi @@ -1418,16 +1585,16 @@ toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmx \ toplevel/coqinit.cmi toplevel/coqtop.cmo: toplevel/cerrors.cmi config/coq_config.cmi \ toplevel/coqinit.cmi library/lib.cmi library/library.cmi \ - toplevel/mltop.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi lib/pp.cmi lib/profile.cmi \ - library/states.cmi lib/system.cmi toplevel/toplevel.cmi \ - toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi toplevel/coqtop.cmi + toplevel/mltop.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ + lib/pp.cmi lib/profile.cmi library/states.cmi lib/system.cmi \ + toplevel/toplevel.cmi toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi \ + toplevel/coqtop.cmi toplevel/coqtop.cmx: toplevel/cerrors.cmx config/coq_config.cmx \ toplevel/coqinit.cmx library/lib.cmx library/library.cmx \ - toplevel/mltop.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx lib/pp.cmx lib/profile.cmx \ - library/states.cmx lib/system.cmx toplevel/toplevel.cmx \ - toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx toplevel/coqtop.cmi + toplevel/mltop.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ + lib/pp.cmx lib/profile.cmx library/states.cmx lib/system.cmx \ + toplevel/toplevel.cmx toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx \ + toplevel/coqtop.cmi toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \ kernel/cooking.cmi kernel/declarations.cmi library/declare.cmi \ kernel/environ.cmi library/global.cmi library/impargs.cmi \ @@ -1456,28 +1623,30 @@ toplevel/himsg.cmo: parsing/ast.cmi pretyping/cases.cmi kernel/environ.cmi \ library/global.cmi kernel/indtypes.cmi kernel/inductive.cmi \ proofs/logic.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ lib/pp.cmi pretyping/pretype_errors.cmi parsing/printer.cmi \ - kernel/reduction.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ + kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ pretyping/termops.cmi kernel/type_errors.cmi lib/util.cmi \ toplevel/himsg.cmi toplevel/himsg.cmx: parsing/ast.cmx pretyping/cases.cmx kernel/environ.cmx \ library/global.cmx kernel/indtypes.cmx kernel/inductive.cmx \ proofs/logic.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ lib/pp.cmx pretyping/pretype_errors.cmx parsing/printer.cmx \ - kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \ + kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \ toplevel/himsg.cmi toplevel/line_oriented_parser.cmo: toplevel/line_oriented_parser.cmi toplevel/line_oriented_parser.cmx: toplevel/line_oriented_parser.cmi toplevel/metasyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \ parsing/coqast.cmi parsing/egrammar.cmi parsing/esyntax.cmi \ - parsing/extend.cmi library/lib.cmi library/libobject.cmi \ - library/library.cmi parsing/pcoq.cmi lib/pp.cmi library/summary.cmi \ - lib/util.cmi toplevel/metasyntax.cmi + parsing/extend.cmi parsing/genarg.cmi library/global.cmi library/lib.cmi \ + library/libobject.cmi library/library.cmi library/nametab.cmi \ + parsing/pcoq.cmi lib/pp.cmi library/summary.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo toplevel/metasyntax.cmi toplevel/metasyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \ parsing/coqast.cmx parsing/egrammar.cmx parsing/esyntax.cmx \ - parsing/extend.cmx library/lib.cmx library/libobject.cmx \ - library/library.cmx parsing/pcoq.cmx lib/pp.cmx library/summary.cmx \ - lib/util.cmx toplevel/metasyntax.cmi + parsing/extend.cmx parsing/genarg.cmx library/global.cmx library/lib.cmx \ + library/libobject.cmx library/library.cmx library/nametab.cmx \ + parsing/pcoq.cmx lib/pp.cmx library/summary.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx toplevel/metasyntax.cmi toplevel/minicoq.cmo: kernel/declarations.cmi toplevel/fhimsg.cmi \ parsing/g_minicoq.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \ kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \ @@ -1494,11 +1663,11 @@ toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \ lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx toplevel/mltop.cmi toplevel/protectedtoplevel.cmo: toplevel/cerrors.cmi \ toplevel/line_oriented_parser.cmi parsing/pcoq.cmi lib/pp.cmi \ - toplevel/vernac.cmi toplevel/vernacinterp.cmi \ + toplevel/vernac.cmi toplevel/vernacexpr.cmo \ toplevel/protectedtoplevel.cmi toplevel/protectedtoplevel.cmx: toplevel/cerrors.cmx \ toplevel/line_oriented_parser.cmx parsing/pcoq.cmx lib/pp.cmx \ - toplevel/vernac.cmx toplevel/vernacinterp.cmx \ + toplevel/vernac.cmx toplevel/vernacexpr.cmx \ toplevel/protectedtoplevel.cmi toplevel/record.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \ toplevel/command.cmi parsing/coqast.cmi kernel/declarations.cmi \ @@ -1508,7 +1677,7 @@ toplevel/record.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \ library/nametab.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \ pretyping/recordops.cmi kernel/safe_typing.cmi kernel/term.cmi \ pretyping/termops.cmi kernel/type_errors.cmi kernel/typeops.cmi \ - lib/util.cmi toplevel/record.cmi + lib/util.cmi toplevel/vernacexpr.cmo toplevel/record.cmi toplevel/record.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \ toplevel/command.cmx parsing/coqast.cmx kernel/declarations.cmx \ library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \ @@ -1517,7 +1686,7 @@ toplevel/record.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \ library/nametab.cmx lib/options.cmx lib/pp.cmx parsing/printer.cmx \ pretyping/recordops.cmx kernel/safe_typing.cmx kernel/term.cmx \ pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \ - lib/util.cmx toplevel/record.cmi + lib/util.cmx toplevel/vernacexpr.cmx toplevel/record.cmi toplevel/recordobj.cmo: pretyping/classops.cmi library/declare.cmi \ kernel/environ.cmi library/global.cmi pretyping/instantiate.cmi \ library/lib.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \ @@ -1531,67 +1700,75 @@ toplevel/recordobj.cmx: pretyping/classops.cmx library/declare.cmx \ toplevel/toplevel.cmo: parsing/ast.cmi toplevel/cerrors.cmi library/lib.cmi \ toplevel/mltop.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \ proofs/pfedit.cmi lib/pp.cmi toplevel/protectedtoplevel.cmi lib/util.cmi \ - toplevel/vernac.cmi toplevel/vernacinterp.cmi toplevel/toplevel.cmi + toplevel/vernac.cmi toplevel/vernacexpr.cmo toplevel/toplevel.cmi toplevel/toplevel.cmx: parsing/ast.cmx toplevel/cerrors.cmx library/lib.cmx \ toplevel/mltop.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \ proofs/pfedit.cmx lib/pp.cmx toplevel/protectedtoplevel.cmx lib/util.cmx \ - toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi + 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/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ - toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \ - parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ - toplevel/discharge.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ - pretyping/evarutil.cmi pretyping/evd.cmi parsing/extend.cmi \ - library/global.cmi library/goptions.cmi library/impargs.cmi \ - pretyping/inductiveops.cmi library/lib.cmi library/library.cmi \ - toplevel/metasyntax.cmi toplevel/mltop.cmi library/nameops.cmi \ - kernel/names.cmi library/nametab.cmi lib/options.cmi proofs/pfedit.cmi \ - lib/pp.cmi lib/pp_control.cmi parsing/prettyp.cmi parsing/printer.cmi \ + tactics/auto.cmi toplevel/class.cmi pretyping/classops.cmi \ + toplevel/command.cmi parsing/coqast.cmi library/declare.cmi \ + tactics/dhyp.cmi toplevel/discharge.cmi kernel/environ.cmi \ + pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ + library/goptions.cmi library/impargs.cmi pretyping/inductiveops.cmi \ + library/lib.cmi library/library.cmi toplevel/metasyntax.cmi \ + toplevel/mltop.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \ + lib/pp_control.cmi parsing/prettyp.cmi parsing/printer.cmi \ proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \ toplevel/recordobj.cmi proofs/refiner.cmi kernel/safe_typing.cmi \ parsing/search.cmi library/states.cmi pretyping/syntax_def.cmi \ - lib/system.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ + lib/system.cmi tactics/tacinterp.cmi proofs/tacmach.cmi \ pretyping/tacred.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \ kernel/term.cmi parsing/termast.cmi kernel/typeops.cmi kernel/univ.cmi \ - lib/util.cmi toplevel/vernacinterp.cmi toplevel/vernacentries.cmi + lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \ + toplevel/vernacentries.cmi toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ - toplevel/class.cmx pretyping/classops.cmx toplevel/command.cmx \ - parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \ - toplevel/discharge.cmx kernel/environ.cmx proofs/evar_refiner.cmx \ - pretyping/evarutil.cmx pretyping/evd.cmx parsing/extend.cmx \ - library/global.cmx library/goptions.cmx library/impargs.cmx \ - pretyping/inductiveops.cmx library/lib.cmx library/library.cmx \ - toplevel/metasyntax.cmx toplevel/mltop.cmx library/nameops.cmx \ - kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pfedit.cmx \ - lib/pp.cmx lib/pp_control.cmx parsing/prettyp.cmx parsing/printer.cmx \ + tactics/auto.cmx toplevel/class.cmx pretyping/classops.cmx \ + toplevel/command.cmx parsing/coqast.cmx library/declare.cmx \ + tactics/dhyp.cmx toplevel/discharge.cmx kernel/environ.cmx \ + pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \ + library/goptions.cmx library/impargs.cmx pretyping/inductiveops.cmx \ + library/lib.cmx library/library.cmx toplevel/metasyntax.cmx \ + toplevel/mltop.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \ + lib/pp_control.cmx parsing/prettyp.cmx parsing/printer.cmx \ proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \ toplevel/recordobj.cmx proofs/refiner.cmx kernel/safe_typing.cmx \ parsing/search.cmx library/states.cmx pretyping/syntax_def.cmx \ - lib/system.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ + lib/system.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \ pretyping/tacred.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \ kernel/term.cmx parsing/termast.cmx kernel/typeops.cmx kernel/univ.cmx \ - lib/util.cmx toplevel/vernacinterp.cmx toplevel/vernacentries.cmi -toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi \ - toplevel/command.cmi parsing/coqast.cmi lib/dyn.cmi toplevel/himsg.cmi \ - kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \ - proofs/proof_type.cmi proofs/tacinterp.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi -toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \ - toplevel/command.cmx parsing/coqast.cmx lib/dyn.cmx toplevel/himsg.cmx \ - kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ - proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \ - toplevel/vernacinterp.cmi + lib/util.cmx toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx \ + toplevel/vernacentries.cmi +toplevel/vernacexpr.cmo: parsing/ast.cmi parsing/coqast.cmi \ + parsing/extend.cmi parsing/genarg.cmi library/goptions.cmi \ + kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \ + proofs/tacexpr.cmo lib/util.cmi +toplevel/vernacexpr.cmx: parsing/ast.cmx parsing/coqast.cmx \ + parsing/extend.cmx parsing/genarg.cmx library/goptions.cmx \ + kernel/names.cmx library/nametab.cmx proofs/proof_type.cmx \ + proofs/tacexpr.cmx lib/util.cmx +toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi \ + parsing/extend.cmi toplevel/himsg.cmi kernel/names.cmi lib/options.cmi \ + lib/pp.cmi proofs/proof_type.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \ + lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi +toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \ + parsing/extend.cmx toplevel/himsg.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: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \ - pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - toplevel/vernac.cmi + pretyping/termops.cmi lib/util.cmi toplevel/vernacentries.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \ - pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - toplevel/vernac.cmi + pretyping/termops.cmx lib/util.cmx toplevel/vernacentries.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ contrib/correctness/past.cmi contrib/correctness/penv.cmi \ contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ @@ -1610,14 +1787,14 @@ contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \ contrib/correctness/past.cmi contrib/correctness/pmisc.cmi \ pretyping/rawterm.cmi toplevel/record.cmi kernel/sign.cmi kernel/term.cmi \ pretyping/termops.cmi kernel/typeops.cmi lib/util.cmi \ - contrib/correctness/pcic.cmi + toplevel/vernacexpr.cmo contrib/correctness/pcic.cmi contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \ library/declare.cmx pretyping/detyping.cmx library/global.cmx \ kernel/indtypes.cmx kernel/names.cmx library/nametab.cmx \ contrib/correctness/past.cmi contrib/correctness/pmisc.cmx \ pretyping/rawterm.cmx toplevel/record.cmx kernel/sign.cmx kernel/term.cmx \ pretyping/termops.cmx kernel/typeops.cmx lib/util.cmx \ - contrib/correctness/pcic.cmi + toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ @@ -1725,9 +1902,10 @@ contrib/correctness/prename.cmx: toplevel/himsg.cmx library/nameops.cmx \ kernel/names.cmx contrib/correctness/pmisc.cmx lib/pp.cmx lib/util.cmx \ contrib/correctness/prename.cmi contrib/correctness/psyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \ - parsing/coqast.cmi library/declare.cmi lib/dyn.cmi pretyping/evd.cmi \ - parsing/g_zsyntax.cmi library/global.cmi toplevel/himsg.cmi \ - library/nameops.cmi kernel/names.cmi lib/options.cmi \ + parsing/coqast.cmi library/declare.cmi pretyping/evd.cmi \ + parsing/extend.cmi parsing/g_zsyntax.cmi parsing/genarg.cmi \ + library/global.cmi toplevel/himsg.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/options.cmi \ contrib/correctness/past.cmi contrib/correctness/pcicenv.cmi \ parsing/pcoq.cmi contrib/correctness/pdb.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ @@ -1735,13 +1913,14 @@ contrib/correctness/psyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \ contrib/correctness/prename.cmi contrib/correctness/ptactic.cmi \ contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmi \ contrib/correctness/putil.cmi kernel/reduction.cmi kernel/safe_typing.cmi \ - proofs/tacinterp.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \ - toplevel/vernac.cmi toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \ - contrib/correctness/psyntax.cmi + tactics/tacinterp.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \ + toplevel/vernac.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacinterp.cmi contrib/correctness/psyntax.cmi contrib/correctness/psyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \ - parsing/coqast.cmx library/declare.cmx lib/dyn.cmx pretyping/evd.cmx \ - parsing/g_zsyntax.cmx library/global.cmx toplevel/himsg.cmx \ - library/nameops.cmx kernel/names.cmx lib/options.cmx \ + parsing/coqast.cmx library/declare.cmx pretyping/evd.cmx \ + parsing/extend.cmx parsing/g_zsyntax.cmx parsing/genarg.cmx \ + library/global.cmx toplevel/himsg.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/options.cmx \ contrib/correctness/past.cmi contrib/correctness/pcicenv.cmx \ parsing/pcoq.cmx contrib/correctness/pdb.cmx \ contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \ @@ -1749,12 +1928,13 @@ contrib/correctness/psyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \ contrib/correctness/prename.cmx contrib/correctness/ptactic.cmx \ contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmx \ contrib/correctness/putil.cmx kernel/reduction.cmx kernel/safe_typing.cmx \ - proofs/tacinterp.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \ - toplevel/vernac.cmx toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \ - contrib/correctness/psyntax.cmi -contrib/correctness/ptactic.cmo: library/declare.cmi tactics/equality.cmi \ - pretyping/evd.cmi library/global.cmi kernel/names.cmi library/nametab.cmi \ - lib/options.cmi contrib/correctness/past.cmi pretyping/pattern.cmi \ + tactics/tacinterp.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \ + toplevel/vernac.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacinterp.cmx contrib/correctness/psyntax.cmi +contrib/correctness/ptactic.cmo: tactics/equality.cmi pretyping/evd.cmi \ + tactics/extratactics.cmi library/global.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/options.cmi \ + contrib/correctness/past.cmi pretyping/pattern.cmi \ contrib/correctness/pcic.cmi contrib/correctness/pdb.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ contrib/correctness/perror.cmi proofs/pfedit.cmi \ @@ -1763,13 +1943,13 @@ contrib/correctness/ptactic.cmo: library/declare.cmi tactics/equality.cmi \ contrib/correctness/prename.cmi pretyping/pretyping.cmi \ parsing/printer.cmi contrib/correctness/ptyping.cmi \ contrib/correctness/putil.cmi contrib/correctness/pwp.cmi \ - kernel/reduction.cmi tactics/refine.cmi proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/termops.cmi lib/util.cmi toplevel/vernacentries.cmi \ - toplevel/vernacinterp.cmi contrib/correctness/ptactic.cmi -contrib/correctness/ptactic.cmx: library/declare.cmx tactics/equality.cmx \ - pretyping/evd.cmx library/global.cmx kernel/names.cmx library/nametab.cmx \ - lib/options.cmx contrib/correctness/past.cmi pretyping/pattern.cmx \ + kernel/reduction.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ + toplevel/vernacentries.cmi contrib/correctness/ptactic.cmi +contrib/correctness/ptactic.cmx: tactics/equality.cmx pretyping/evd.cmx \ + tactics/extratactics.cmx library/global.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/options.cmx \ + contrib/correctness/past.cmi pretyping/pattern.cmx \ contrib/correctness/pcic.cmx contrib/correctness/pdb.cmx \ contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \ contrib/correctness/perror.cmx proofs/pfedit.cmx \ @@ -1778,10 +1958,9 @@ contrib/correctness/ptactic.cmx: library/declare.cmx tactics/equality.cmx \ contrib/correctness/prename.cmx pretyping/pretyping.cmx \ parsing/printer.cmx contrib/correctness/ptyping.cmx \ contrib/correctness/putil.cmx contrib/correctness/pwp.cmx \ - kernel/reduction.cmx tactics/refine.cmx proofs/tacmach.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/termops.cmx lib/util.cmx toplevel/vernacentries.cmx \ - toplevel/vernacinterp.cmx contrib/correctness/ptactic.cmi + kernel/reduction.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ + toplevel/vernacentries.cmx contrib/correctness/ptactic.cmi contrib/correctness/ptyping.cmo: parsing/ast.cmi parsing/astterm.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ toplevel/himsg.cmi kernel/names.cmi contrib/correctness/past.cmi \ @@ -1880,6 +2059,16 @@ contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \ lib/pp.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ library/summary.cmx contrib/extraction/table.cmx kernel/term.cmx \ pretyping/termops.cmx lib/util.cmx contrib/extraction/extraction.cmi +contrib/extraction/g_extraction.cmo: toplevel/cerrors.cmi \ + parsing/egrammar.cmi contrib/extraction/extract_env.cmi \ + parsing/genarg.cmi parsing/pcoq.cmi lib/pp.cmi \ + contrib/extraction/table.cmi tactics/tacinterp.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi +contrib/extraction/g_extraction.cmx: toplevel/cerrors.cmx \ + parsing/egrammar.cmx contrib/extraction/extract_env.cmx \ + parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \ + contrib/extraction/table.cmx tactics/tacinterp.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx contrib/extraction/haskell.cmo: contrib/extraction/miniml.cmi \ contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \ library/nametab.cmi contrib/extraction/ocaml.cmi lib/options.cmi \ @@ -1908,40 +2097,56 @@ contrib/extraction/ocaml.cmx: contrib/extraction/miniml.cmi \ library/nametab.cmx lib/options.cmx lib/pp.cmx \ contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \ contrib/extraction/ocaml.cmi -contrib/extraction/table.cmo: kernel/declarations.cmi library/global.cmi \ - library/goptions.cmi library/lib.cmi library/libobject.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \ - library/summary.cmi kernel/term.cmi lib/util.cmi \ +contrib/extraction/table.cmo: kernel/declarations.cmi parsing/extend.cmi \ + library/global.cmi library/goptions.cmi library/lib.cmi \ + library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + parsing/printer.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \ toplevel/vernacinterp.cmi contrib/extraction/table.cmi -contrib/extraction/table.cmx: kernel/declarations.cmx library/global.cmx \ - library/goptions.cmx library/lib.cmx library/libobject.cmx \ - kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \ - library/summary.cmx kernel/term.cmx lib/util.cmx \ +contrib/extraction/table.cmx: kernel/declarations.cmx parsing/extend.cmx \ + library/global.cmx library/goptions.cmx library/lib.cmx \ + library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + parsing/printer.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \ toplevel/vernacinterp.cmx contrib/extraction/table.cmi -contrib/field/field.cmo: parsing/astterm.cmi parsing/coqast.cmi \ - library/declare.cmi pretyping/evd.cmi library/global.cmi library/lib.cmi \ - library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ - proofs/proof_type.cmi contrib/ring/quote.cmo pretyping/reductionops.cmi \ - contrib/ring/ring.cmo library/summary.cmi proofs/tacinterp.cmi \ - proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ +contrib/field/field.cmo: parsing/astterm.cmi toplevel/cerrors.cmi \ + parsing/coqast.cmi library/declare.cmi parsing/egrammar.cmi \ + pretyping/evd.cmi parsing/extend.cmi parsing/genarg.cmi \ + library/global.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \ + library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \ + proofs/proof_type.cmi contrib/ring/quote.cmo pretyping/rawterm.cmi \ + pretyping/reductionops.cmi proofs/refiner.cmi contrib/ring/ring.cmo \ + library/summary.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \ + proofs/tacmach.cmi tactics/tacticals.cmi kernel/term.cmi \ + pretyping/typing.cmi lib/util.cmi toplevel/vernacexpr.cmo \ toplevel/vernacinterp.cmi -contrib/field/field.cmx: parsing/astterm.cmx parsing/coqast.cmx \ - library/declare.cmx pretyping/evd.cmx library/global.cmx library/lib.cmx \ - library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ - proofs/proof_type.cmx contrib/ring/quote.cmx pretyping/reductionops.cmx \ - contrib/ring/ring.cmx library/summary.cmx proofs/tacinterp.cmx \ - proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ +contrib/field/field.cmx: parsing/astterm.cmx toplevel/cerrors.cmx \ + parsing/coqast.cmx library/declare.cmx parsing/egrammar.cmx \ + pretyping/evd.cmx parsing/extend.cmx parsing/genarg.cmx \ + library/global.cmx library/lib.cmx library/libobject.cmx kernel/names.cmx \ + library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \ + proofs/proof_type.cmx contrib/ring/quote.cmx pretyping/rawterm.cmx \ + pretyping/reductionops.cmx proofs/refiner.cmx contrib/ring/ring.cmx \ + library/summary.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx kernel/term.cmx \ + pretyping/typing.cmx lib/util.cmx toplevel/vernacexpr.cmx \ toplevel/vernacinterp.cmx contrib/fourier/fourierR.cmo: parsing/astterm.cmi proofs/clenv.cmi \ - tactics/equality.cmi pretyping/evd.cmi contrib/fourier/fourier.cmo \ - library/global.cmi kernel/names.cmi parsing/pcoq.cmi \ - contrib/ring/ring.cmo proofs/tacmach.cmi tactics/tactics.cmi \ - kernel/term.cmi + tactics/contradiction.cmi tactics/equality.cmi pretyping/evd.cmi \ + contrib/fourier/fourier.cmo library/global.cmi kernel/names.cmi \ + parsing/pcoq.cmi contrib/ring/ring.cmo proofs/tacmach.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ + toplevel/vernacexpr.cmo contrib/fourier/fourierR.cmx: parsing/astterm.cmx proofs/clenv.cmx \ - tactics/equality.cmx pretyping/evd.cmx contrib/fourier/fourier.cmx \ - library/global.cmx kernel/names.cmx parsing/pcoq.cmx \ - contrib/ring/ring.cmx proofs/tacmach.cmx tactics/tactics.cmx \ - kernel/term.cmx + tactics/contradiction.cmx tactics/equality.cmx pretyping/evd.cmx \ + contrib/fourier/fourier.cmx library/global.cmx kernel/names.cmx \ + parsing/pcoq.cmx contrib/ring/ring.cmx proofs/tacmach.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ + toplevel/vernacexpr.cmx +contrib/fourier/g_fourier.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \ + contrib/fourier/fourierR.cmo parsing/pcoq.cmi lib/pp.cmi \ + parsing/pptactic.cmi proofs/refiner.cmi +contrib/fourier/g_fourier.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ + contrib/fourier/fourierR.cmx parsing/pcoq.cmx lib/pp.cmx \ + parsing/pptactic.cmx proofs/refiner.cmx contrib/interface/blast.cmo: parsing/astterm.cmi tactics/auto.cmi \ proofs/clenv.cmi toplevel/command.cmi contrib/interface/ctast.cmo \ kernel/declarations.cmi library/declare.cmi tactics/eauto.cmo \ @@ -1950,11 +2155,11 @@ contrib/interface/blast.cmo: parsing/astterm.cmi tactics/auto.cmi \ tactics/hipattern.cmi kernel/inductive.cmi proofs/logic.cmi \ library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi \ contrib/interface/pbp.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \ - kernel/sign.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ + parsing/pptactic.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ + proofs/refiner.cmi kernel/sign.cmi proofs/tacmach.cmi \ + pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \ contrib/interface/blast.cmi contrib/interface/blast.cmx: parsing/astterm.cmx tactics/auto.cmx \ @@ -1965,11 +2170,11 @@ contrib/interface/blast.cmx: parsing/astterm.cmx tactics/auto.cmx \ tactics/hipattern.cmx kernel/inductive.cmx proofs/logic.cmx \ library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx \ contrib/interface/pbp.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - pretyping/rawterm.cmx kernel/reduction.cmx proofs/refiner.cmx \ - kernel/sign.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ + parsing/pptactic.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ + proofs/refiner.cmx kernel/sign.cmx proofs/tacmach.cmx \ + pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \ contrib/interface/blast.cmi contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ @@ -1977,69 +2182,77 @@ contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ pretyping/classops.cmi toplevel/command.cmi parsing/coqast.cmi \ contrib/interface/ctast.cmo contrib/interface/dad.cmi \ contrib/interface/debug_tac.cmi kernel/declarations.cmi \ - library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \ - library/global.cmi contrib/interface/history.cmi library/lib.cmi \ - library/libobject.cmi library/library.cmi \ - toplevel/line_oriented_parser.cmi toplevel/mltop.cmi \ + library/declare.cmi parsing/egrammar.cmi kernel/environ.cmi \ + pretyping/evd.cmi parsing/genarg.cmi library/global.cmi \ + contrib/interface/history.cmi library/lib.cmi library/libobject.cmi \ + library/library.cmi toplevel/line_oriented_parser.cmi toplevel/mltop.cmi \ contrib/interface/name_to_ast.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi contrib/interface/pbp.cmi proofs/pfedit.cmi \ - lib/pp.cmi pretyping/pretyping.cmi parsing/printer.cmi \ + library/nametab.cmi contrib/interface/pbp.cmi parsing/pcoq.cmi \ + proofs/pfedit.cmi lib/pp.cmi parsing/pptactic.cmi pretyping/pretyping.cmi \ proofs/proof_trees.cmi proofs/proof_type.cmi \ toplevel/protectedtoplevel.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ - parsing/search.cmi contrib/interface/showproof.cmi \ - contrib/interface/showproof_ct.cmo proofs/tacinterp.cmi \ - proofs/tacmach.cmi pretyping/tacred.cmi kernel/term.cmi \ + proofs/refiner.cmi parsing/search.cmi contrib/interface/showproof.cmi \ + contrib/interface/showproof_ct.cmo proofs/tacexpr.cmo \ + tactics/tacinterp.cmi proofs/tacmach.cmi kernel/term.cmi \ parsing/termast.cmi contrib/interface/translate.cmi lib/util.cmi \ - toplevel/vernac.cmi toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \ - contrib/interface/vtp.cmi contrib/interface/xlate.cmi + toplevel/vernac.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacinterp.cmi contrib/interface/vtp.cmi \ + contrib/interface/xlate.cmi contrib/interface/centaur.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \ parsing/astterm.cmx contrib/interface/blast.cmx toplevel/cerrors.cmx \ pretyping/classops.cmx toplevel/command.cmx parsing/coqast.cmx \ contrib/interface/ctast.cmx contrib/interface/dad.cmx \ contrib/interface/debug_tac.cmx kernel/declarations.cmx \ - library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \ - library/global.cmx contrib/interface/history.cmx library/lib.cmx \ - library/libobject.cmx library/library.cmx \ - toplevel/line_oriented_parser.cmx toplevel/mltop.cmx \ + library/declare.cmx parsing/egrammar.cmx kernel/environ.cmx \ + pretyping/evd.cmx parsing/genarg.cmx library/global.cmx \ + contrib/interface/history.cmx library/lib.cmx library/libobject.cmx \ + library/library.cmx toplevel/line_oriented_parser.cmx toplevel/mltop.cmx \ contrib/interface/name_to_ast.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx contrib/interface/pbp.cmx proofs/pfedit.cmx \ - lib/pp.cmx pretyping/pretyping.cmx parsing/printer.cmx \ + library/nametab.cmx contrib/interface/pbp.cmx parsing/pcoq.cmx \ + proofs/pfedit.cmx lib/pp.cmx parsing/pptactic.cmx pretyping/pretyping.cmx \ proofs/proof_trees.cmx proofs/proof_type.cmx \ toplevel/protectedtoplevel.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ - parsing/search.cmx contrib/interface/showproof.cmx \ - contrib/interface/showproof_ct.cmx proofs/tacinterp.cmx \ - proofs/tacmach.cmx pretyping/tacred.cmx kernel/term.cmx \ + proofs/refiner.cmx parsing/search.cmx contrib/interface/showproof.cmx \ + contrib/interface/showproof_ct.cmx proofs/tacexpr.cmx \ + tactics/tacinterp.cmx proofs/tacmach.cmx kernel/term.cmx \ parsing/termast.cmx contrib/interface/translate.cmx lib/util.cmx \ - toplevel/vernac.cmx toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \ - contrib/interface/vtp.cmx contrib/interface/xlate.cmx + toplevel/vernac.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacinterp.cmx contrib/interface/vtp.cmx \ + contrib/interface/xlate.cmx contrib/interface/ctast.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \ kernel/names.cmi contrib/interface/ctast.cmx: parsing/ast.cmx parsing/coqast.cmx lib/dyn.cmx \ kernel/names.cmx -contrib/interface/dad.cmo: parsing/astterm.cmi contrib/interface/ctast.cmo \ - kernel/environ.cmi pretyping/evd.cmi library/global.cmi kernel/names.cmi \ +contrib/interface/dad.cmo: parsing/astterm.cmi parsing/coqast.cmi \ + contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evd.cmi \ + parsing/genarg.cmi library/global.cmi kernel/names.cmi \ library/nametab.cmi contrib/interface/paths.cmi pretyping/pattern.cmi \ lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - pretyping/rawterm.cmi kernel/reduction.cmi proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi contrib/interface/dad.cmi -contrib/interface/dad.cmx: parsing/astterm.cmx contrib/interface/ctast.cmx \ - kernel/environ.cmx pretyping/evd.cmx library/global.cmx kernel/names.cmx \ + pretyping/rawterm.cmi kernel/reduction.cmi proofs/tacexpr.cmo \ + proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \ + contrib/interface/dad.cmi +contrib/interface/dad.cmx: parsing/astterm.cmx parsing/coqast.cmx \ + contrib/interface/ctast.cmx kernel/environ.cmx pretyping/evd.cmx \ + parsing/genarg.cmx library/global.cmx kernel/names.cmx \ library/nametab.cmx contrib/interface/paths.cmx pretyping/pattern.cmx \ lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - pretyping/rawterm.cmx kernel/reduction.cmx proofs/tacmach.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx contrib/interface/dad.cmi + pretyping/rawterm.cmx kernel/reduction.cmx proofs/tacexpr.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx \ + contrib/interface/dad.cmi contrib/interface/debug_tac.cmo: parsing/ast.cmi toplevel/cerrors.cmi \ - parsing/coqast.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ - lib/util.cmi contrib/interface/debug_tac.cmi + parsing/coqast.cmi parsing/genarg.cmi lib/pp.cmi parsing/pptactic.cmi \ + proofs/proof_trees.cmi proofs/proof_type.cmi proofs/refiner.cmi \ + proofs/tacexpr.cmo tactics/tacinterp.cmi proofs/tacmach.cmi \ + tactics/tacticals.cmi lib/util.cmi contrib/interface/debug_tac.cmi contrib/interface/debug_tac.cmx: parsing/ast.cmx toplevel/cerrors.cmx \ - parsing/coqast.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ - lib/util.cmx contrib/interface/debug_tac.cmi + parsing/coqast.cmx parsing/genarg.cmx lib/pp.cmx parsing/pptactic.cmx \ + proofs/proof_trees.cmx proofs/proof_type.cmx proofs/refiner.cmx \ + proofs/tacexpr.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \ + tactics/tacticals.cmx lib/util.cmx contrib/interface/debug_tac.cmi contrib/interface/history.cmo: contrib/interface/paths.cmi \ contrib/interface/history.cmi contrib/interface/history.cmx: contrib/interface/paths.cmx \ @@ -2053,7 +2266,7 @@ contrib/interface/name_to_ast.cmo: parsing/ast.cmi pretyping/classops.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ parsing/prettyp.cmi kernel/reduction.cmi kernel/sign.cmi \ pretyping/syntax_def.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \ - contrib/interface/name_to_ast.cmi + toplevel/vernacexpr.cmo contrib/interface/name_to_ast.cmi contrib/interface/name_to_ast.cmx: parsing/ast.cmx pretyping/classops.cmx \ parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \ kernel/environ.cmx library/global.cmx library/impargs.cmx \ @@ -2061,40 +2274,42 @@ contrib/interface/name_to_ast.cmx: parsing/ast.cmx pretyping/classops.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ parsing/prettyp.cmx kernel/reduction.cmx kernel/sign.cmx \ pretyping/syntax_def.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \ - contrib/interface/name_to_ast.cmi + toplevel/vernacexpr.cmx contrib/interface/name_to_ast.cmi contrib/interface/parse.cmo: contrib/interface/ascent.cmi \ toplevel/cerrors.cmi config/coq_config.cmi contrib/interface/ctast.cmo \ parsing/esyntax.cmi library/libobject.cmi library/library.cmi \ - contrib/interface/line_parser.cmi toplevel/metasyntax.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi \ - lib/pp.cmi lib/system.cmi lib/util.cmi contrib/interface/vtp.cmi \ - contrib/interface/xlate.cmi + contrib/interface/line_parser.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi lib/system.cmi \ + lib/util.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \ + contrib/interface/vtp.cmi contrib/interface/xlate.cmi contrib/interface/parse.cmx: contrib/interface/ascent.cmi \ toplevel/cerrors.cmx config/coq_config.cmx contrib/interface/ctast.cmx \ parsing/esyntax.cmx library/libobject.cmx library/library.cmx \ - contrib/interface/line_parser.cmx toplevel/metasyntax.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx \ - lib/pp.cmx lib/system.cmx lib/util.cmx contrib/interface/vtp.cmx \ - contrib/interface/xlate.cmx + contrib/interface/line_parser.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx lib/system.cmx \ + lib/util.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \ + contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/paths.cmo: contrib/interface/paths.cmi contrib/interface/paths.cmx: contrib/interface/paths.cmi -contrib/interface/pbp.cmo: parsing/astterm.cmi parsing/coqlib.cmi \ - contrib/interface/ctast.cmo library/declare.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \ - proofs/logic.cmi kernel/names.cmi library/nametab.cmi \ - pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/pretyping.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ - kernel/reduction.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ +contrib/interface/pbp.cmo: parsing/astterm.cmi parsing/coqast.cmi \ + parsing/coqlib.cmi contrib/interface/ctast.cmo library/declare.cmi \ + kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ + tactics/hipattern.cmi proofs/logic.cmi kernel/names.cmi \ + library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \ + pretyping/pretyping.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi kernel/reduction.cmi proofs/tacexpr.cmo \ + tactics/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi \ pretyping/typing.cmi lib/util.cmi contrib/interface/pbp.cmi -contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqlib.cmx \ - contrib/interface/ctast.cmx library/declare.cmx kernel/environ.cmx \ - pretyping/evd.cmx library/global.cmx tactics/hipattern.cmx \ - proofs/logic.cmx kernel/names.cmx library/nametab.cmx \ - pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/pretyping.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ - kernel/reduction.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ +contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqast.cmx \ + parsing/coqlib.cmx contrib/interface/ctast.cmx library/declare.cmx \ + kernel/environ.cmx pretyping/evd.cmx library/global.cmx \ + tactics/hipattern.cmx proofs/logic.cmx kernel/names.cmx \ + library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \ + pretyping/pretyping.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + pretyping/rawterm.cmx kernel/reduction.cmx proofs/tacexpr.cmx \ + tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx parsing/termast.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 \ @@ -2106,24 +2321,28 @@ contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \ proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \ - kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ - kernel/inductive.cmi pretyping/inductiveops.cmi library/nameops.cmi \ - kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \ - contrib/interface/showproof_ct.cmo kernel/sign.cmi proofs/tacmach.cmi \ - kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \ - contrib/interface/translate.cmi pretyping/typing.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi contrib/interface/showproof.cmi + kernel/environ.cmi pretyping/evd.cmi parsing/genarg.cmi \ + library/global.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ + library/nameops.cmi kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi \ + parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi pretyping/reductionops.cmi \ + contrib/interface/showproof_ct.cmo kernel/sign.cmi proofs/tacexpr.cmo \ + proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \ + pretyping/termops.cmi contrib/interface/translate.cmi \ + pretyping/typing.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + contrib/interface/showproof.cmi contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \ proofs/clenv.cmx parsing/coqast.cmx kernel/declarations.cmx \ - kernel/environ.cmx pretyping/evd.cmx library/global.cmx \ - kernel/inductive.cmx pretyping/inductiveops.cmx library/nameops.cmx \ - kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \ - contrib/interface/showproof_ct.cmx kernel/sign.cmx proofs/tacmach.cmx \ - kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \ - contrib/interface/translate.cmx pretyping/typing.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx contrib/interface/showproof.cmi + kernel/environ.cmx pretyping/evd.cmx parsing/genarg.cmx \ + library/global.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ + library/nameops.cmx kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx \ + parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + pretyping/rawterm.cmx pretyping/reductionops.cmx \ + contrib/interface/showproof_ct.cmx kernel/sign.cmx proofs/tacexpr.cmx \ + proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \ + pretyping/termops.cmx contrib/interface/translate.cmx \ + pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + contrib/interface/showproof.cmi contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/libobject.cmi library/library.cmi \ @@ -2143,11 +2362,17 @@ contrib/interface/vtp.cmo: contrib/interface/ascent.cmi \ contrib/interface/vtp.cmx: contrib/interface/ascent.cmi \ contrib/interface/vtp.cmi contrib/interface/xlate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ - contrib/interface/ctast.cmo library/nameops.cmi kernel/names.cmi \ - lib/util.cmi contrib/interface/xlate.cmi + parsing/astterm.cmi parsing/coqast.cmi contrib/interface/ctast.cmo \ + tactics/extraargs.cmi parsing/genarg.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \ + proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo \ + contrib/interface/xlate.cmi contrib/interface/xlate.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \ - contrib/interface/ctast.cmx library/nameops.cmx kernel/names.cmx \ - lib/util.cmx contrib/interface/xlate.cmi + parsing/astterm.cmx parsing/coqast.cmx contrib/interface/ctast.cmx \ + tactics/extraargs.cmx parsing/genarg.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx pretyping/rawterm.cmx \ + proofs/tacexpr.cmx lib/util.cmx toplevel/vernacexpr.cmx \ + contrib/interface/xlate.cmi contrib/jprover/jall.cmo: contrib/jprover/jlogic.cmi \ contrib/jprover/jterm.cmi contrib/jprover/jtunify.cmi \ contrib/jprover/opname.cmi contrib/jprover/jall.cmi @@ -2158,20 +2383,24 @@ contrib/jprover/jlogic.cmo: contrib/jprover/jterm.cmi \ contrib/jprover/opname.cmi contrib/jprover/jlogic.cmi contrib/jprover/jlogic.cmx: contrib/jprover/jterm.cmx \ contrib/jprover/opname.cmx contrib/jprover/jlogic.cmi -contrib/jprover/jprover.cmo: proofs/clenv.cmi library/global.cmi \ - tactics/hipattern.cmi contrib/jprover/jall.cmi contrib/jprover/jlogic.cmi \ - contrib/jprover/jterm.cmi kernel/names.cmi pretyping/pattern.cmi \ - lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \ - pretyping/reductionops.cmi tactics/tacentries.cmi proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/termops.cmi lib/util.cmi -contrib/jprover/jprover.cmx: proofs/clenv.cmx library/global.cmx \ - tactics/hipattern.cmx contrib/jprover/jall.cmx contrib/jprover/jlogic.cmx \ - contrib/jprover/jterm.cmx kernel/names.cmx pretyping/pattern.cmx \ - lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \ - pretyping/reductionops.cmx tactics/tacentries.cmx proofs/tacmach.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/termops.cmx lib/util.cmx +contrib/jprover/jprover.cmo: toplevel/cerrors.cmi proofs/clenv.cmi \ + parsing/egrammar.cmi parsing/genarg.cmi library/global.cmi \ + tactics/hiddentac.cmi tactics/hipattern.cmi contrib/jprover/jall.cmi \ + contrib/jprover/jlogic.cmi contrib/jprover/jterm.cmi kernel/names.cmi \ + pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \ + parsing/printer.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ + kernel/reduction.cmi pretyping/reductionops.cmi proofs/refiner.cmi \ + proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi pretyping/termops.cmi lib/util.cmi +contrib/jprover/jprover.cmx: toplevel/cerrors.cmx proofs/clenv.cmx \ + parsing/egrammar.cmx parsing/genarg.cmx library/global.cmx \ + tactics/hiddentac.cmx tactics/hipattern.cmx contrib/jprover/jall.cmx \ + contrib/jprover/jlogic.cmx contrib/jprover/jterm.cmx kernel/names.cmx \ + pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \ + parsing/printer.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ + kernel/reduction.cmx pretyping/reductionops.cmx proofs/refiner.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx pretyping/termops.cmx lib/util.cmx contrib/jprover/jterm.cmo: contrib/jprover/opname.cmi \ contrib/jprover/jterm.cmi contrib/jprover/jterm.cmx: contrib/jprover/opname.cmx \ @@ -2181,34 +2410,56 @@ contrib/jprover/jtunify.cmx: contrib/jprover/jtunify.cmi contrib/jprover/opname.cmo: contrib/jprover/opname.cmi contrib/jprover/opname.cmx: contrib/jprover/opname.cmi contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \ - kernel/closure.cmi parsing/coqlib.cmi kernel/declarations.cmi \ - library/declare.cmi kernel/environ.cmi tactics/equality.cmi \ - proofs/evar_refiner.cmi library/global.cmi kernel/inductive.cmi \ - proofs/logic.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \ + kernel/closure.cmi tactics/contradiction.cmi parsing/coqlib.cmi \ + kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ + tactics/equality.cmi proofs/evar_refiner.cmi library/global.cmi \ + library/goptions.cmi kernel/inductive.cmi proofs/logic.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi \ contrib/omega/omega.cmo lib/pp.cmi parsing/printer.cmi \ - proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \ - proofs/tacmach.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/termops.cmi lib/util.cmi + proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ + kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi contrib/omega/coq_omega.cmx: parsing/ast.cmx proofs/clenv.cmx \ - kernel/closure.cmx parsing/coqlib.cmx kernel/declarations.cmx \ - library/declare.cmx kernel/environ.cmx tactics/equality.cmx \ - proofs/evar_refiner.cmx library/global.cmx kernel/inductive.cmx \ - proofs/logic.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \ + kernel/closure.cmx tactics/contradiction.cmx parsing/coqlib.cmx \ + kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ + tactics/equality.cmx proofs/evar_refiner.cmx library/global.cmx \ + library/goptions.cmx kernel/inductive.cmx proofs/logic.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx \ contrib/omega/omega.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \ - proofs/tacmach.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/termops.cmx lib/util.cmx + proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ + kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx +contrib/omega/g_omega.cmo: toplevel/cerrors.cmi contrib/omega/coq_omega.cmo \ + parsing/egrammar.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \ + proofs/refiner.cmi +contrib/omega/g_omega.cmx: toplevel/cerrors.cmx contrib/omega/coq_omega.cmx \ + parsing/egrammar.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \ + proofs/refiner.cmx contrib/omega/omega.cmo: lib/util.cmi contrib/omega/omega.cmx: lib/util.cmx +contrib/ring/g_quote.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \ + parsing/genarg.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \ + contrib/ring/quote.cmo proofs/refiner.cmi +contrib/ring/g_quote.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ + parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \ + contrib/ring/quote.cmx proofs/refiner.cmx +contrib/ring/g_ring.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \ + parsing/genarg.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \ + contrib/ring/quote.cmo proofs/refiner.cmi contrib/ring/ring.cmo \ + toplevel/vernacinterp.cmi +contrib/ring/g_ring.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ + parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \ + contrib/ring/quote.cmx proofs/refiner.cmx contrib/ring/ring.cmx \ + toplevel/vernacinterp.cmx contrib/ring/quote.cmo: library/declare.cmi kernel/environ.cmi \ library/global.cmi pretyping/instantiate.cmi kernel/names.cmi \ library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi proofs/tacmach.cmi \ + proofs/proof_trees.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi contrib/ring/quote.cmx: library/declare.cmx kernel/environ.cmx \ library/global.cmx pretyping/instantiate.cmx kernel/names.cmx \ library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx proofs/tacmach.cmx \ + proofs/proof_trees.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx contrib/ring/ring.cmo: parsing/astterm.cmi kernel/closure.cmi \ parsing/coqlib.cmi library/declare.cmi tactics/equality.cmi \ @@ -2216,28 +2467,34 @@ contrib/ring/ring.cmo: parsing/astterm.cmi kernel/closure.cmi \ tactics/hipattern.cmi library/lib.cmi library/libobject.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi contrib/ring/quote.cmo \ - pretyping/reductionops.cmi tactics/setoid_replace.cmi library/summary.cmi \ - proofs/tacmach.cmi pretyping/tacred.cmi tactics/tactics.cmi \ - kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi + proofs/proof_trees.cmi contrib/ring/quote.cmo pretyping/reductionops.cmi \ + tactics/setoid_replace.cmi library/summary.cmi proofs/tacexpr.cmo \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi contrib/ring/ring.cmx: parsing/astterm.cmx kernel/closure.cmx \ parsing/coqlib.cmx library/declare.cmx tactics/equality.cmx \ pretyping/evd.cmx library/global.cmx tactics/hiddentac.cmx \ tactics/hipattern.cmx library/lib.cmx library/libobject.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx contrib/ring/quote.cmx \ - pretyping/reductionops.cmx tactics/setoid_replace.cmx library/summary.cmx \ - proofs/tacmach.cmx pretyping/tacred.cmx tactics/tactics.cmx \ - kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx + proofs/proof_trees.cmx contrib/ring/quote.cmx pretyping/reductionops.cmx \ + tactics/setoid_replace.cmx library/summary.cmx proofs/tacexpr.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx contrib/romega/const_omega.cmo: library/declare.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi kernel/term.cmi \ pretyping/termops.cmi lib/util.cmi contrib/romega/const_omega.cmx: library/declare.cmx library/global.cmx \ kernel/names.cmx library/nametab.cmx kernel/term.cmx \ pretyping/termops.cmx lib/util.cmx +contrib/romega/g_romega.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \ + parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi proofs/refiner.cmi \ + contrib/romega/refl_omega.cmo +contrib/romega/g_romega.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ + parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx proofs/refiner.cmx \ + contrib/romega/refl_omega.cmx contrib/romega/refl_omega.cmo: parsing/ast.cmi tactics/auto.cmi \ proofs/clenv.cmi contrib/romega/const_omega.cmo \ contrib/omega/coq_omega.cmo kernel/environ.cmi kernel/inductive.cmi \ @@ -2268,20 +2525,54 @@ contrib/xml/xmlcommand.cmx: kernel/declarations.cmx library/declare.cmx \ kernel/safe_typing.cmx kernel/sign.cmx lib/system.cmx proofs/tacmach.cmx \ kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx \ contrib/xml/xmlcommand.cmi -contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \ - contrib/xml/xmlcommand.cmi -contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \ - contrib/xml/xmlcommand.cmx +contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \ + parsing/extend.cmi parsing/genarg.cmi parsing/pcoq.cmi lib/pp.cmi \ + parsing/pptactic.cmi tactics/tacinterp.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi contrib/xml/xmlcommand.cmi +contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ + parsing/extend.cmx parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \ + parsing/pptactic.cmx tactics/tacinterp.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx contrib/xml/xml.cmo: contrib/xml/xml.cmi contrib/xml/xml.cmx: contrib/xml/xml.cmi tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo tactics/tauto.cmx: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo +tactics/eqdecide.cmo: parsing/grammar.cma +tactics/eqdecide.cmx: parsing/grammar.cma +tactics/extraargs.cmo: parsing/grammar.cma +tactics/extraargs.cmx: parsing/grammar.cma +tactics/extratactics.cmo: parsing/grammar.cma +tactics/extratactics.cmx: parsing/grammar.cma +tactics/eauto.cmo: parsing/grammar.cma +tactics/eauto.cmx: parsing/grammar.cma +contrib/interface/debug_tac.cmo: parsing/grammar.cma +contrib/interface/debug_tac.cmx: parsing/grammar.cma +contrib/interface/centaur.cmo: parsing/grammar.cma +contrib/interface/centaur.cmx: parsing/grammar.cma contrib/correctness/psyntax.cmo: parsing/grammar.cma contrib/correctness/psyntax.cmx: parsing/grammar.cma +contrib/omega/g_omega.cmo: parsing/grammar.cma +contrib/omega/g_omega.cmx: parsing/grammar.cma +contrib/romega/g_romega.cmo: parsing/grammar.cma +contrib/romega/g_romega.cmx: parsing/grammar.cma +contrib/ring/g_quote.cmo: parsing/grammar.cma +contrib/ring/g_quote.cmx: parsing/grammar.cma +contrib/ring/g_ring.cmo: parsing/grammar.cma +contrib/ring/g_ring.cmx: parsing/grammar.cma contrib/field/field.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo contrib/field/field.cmx: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo +contrib/fourier/g_fourier.cmo: parsing/grammar.cma +contrib/fourier/g_fourier.cmx: parsing/grammar.cma +contrib/extraction/g_extraction.cmo: parsing/grammar.cma +contrib/extraction/g_extraction.cmx: parsing/grammar.cma +contrib/xml/xmlentries.cmo: parsing/grammar.cma +contrib/xml/xmlentries.cmx: parsing/grammar.cma +contrib/jprover/jprover.cmo: parsing/grammar.cma +contrib/jprover/jprover.cmx: parsing/grammar.cma parsing/lexer.cmo: parsing/lexer.cmx: +parsing/q_util.cmo: +parsing/q_util.cmx: parsing/q_coqast.cmo: parsing/q_coqast.cmx: parsing/g_prim.cmo: @@ -2304,8 +2595,10 @@ parsing/g_tactic.cmo: parsing/grammar.cma parsing/g_tactic.cmx: parsing/grammar.cma parsing/g_ltac.cmo: parsing/grammar.cma parsing/g_ltac.cmx: parsing/grammar.cma -parsing/extend.cmo: parsing/grammar.cma -parsing/extend.cmx: parsing/grammar.cma +parsing/tacextend.cmo: +parsing/tacextend.cmx: +parsing/vernacextend.cmo: +parsing/vernacextend.cmx: toplevel/mltop.cmo: toplevel/mltop.cmx: lib/pp.cmo: diff --git a/.depend.camlp4 b/.depend.camlp4 index 94a85c9807..bbbdb186cd 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -1,7 +1,22 @@ tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo +tactics/eqdecide.ml: parsing/grammar.cma +tactics/extraargs.ml: parsing/grammar.cma +tactics/extratactics.ml: parsing/grammar.cma +tactics/eauto.ml: parsing/grammar.cma +contrib/interface/debug_tac.ml: parsing/grammar.cma +contrib/interface/centaur.ml: parsing/grammar.cma contrib/correctness/psyntax.ml: parsing/grammar.cma +contrib/omega/g_omega.ml: parsing/grammar.cma +contrib/romega/g_romega.ml: parsing/grammar.cma +contrib/ring/g_quote.ml: parsing/grammar.cma +contrib/ring/g_ring.ml: parsing/grammar.cma contrib/field/field.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo +contrib/fourier/g_fourier.ml: parsing/grammar.cma +contrib/extraction/g_extraction.ml: parsing/grammar.cma +contrib/xml/xmlentries.ml: parsing/grammar.cma +contrib/jprover/jprover.ml: parsing/grammar.cma parsing/lexer.ml: +parsing/q_util.ml: parsing/q_coqast.ml: parsing/g_prim.ml: parsing/pcoq.ml: @@ -13,7 +28,8 @@ parsing/g_cases.ml: parsing/grammar.cma parsing/g_constr.ml: parsing/grammar.cma parsing/g_tactic.ml: parsing/grammar.cma parsing/g_ltac.ml: parsing/grammar.cma -parsing/extend.ml: parsing/grammar.cma +parsing/tacextend.ml: +parsing/vernacextend.ml: toplevel/mltop.ml: lib/pp.ml: contrib/xml/xml.ml: diff --git a/.depend.coq b/.depend.coq index 928dd10deb..df11634755 100644 --- a/.depend.coq +++ b/.depend.coq @@ -1,8 +1,6 @@ -contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v -contrib/jprover/JProver.vo: contrib/jprover/JProver.v +contrib/interface/Centaur.vo: contrib/interface/Centaur.v contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/fourier/Fourier_util.vo contrib/field/Field.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo -contrib/interface/Centaur.vo: contrib/interface/Centaur.v contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/correctness/ProgWf.vo: contrib/correctness/ProgWf.v theories/ZArith/ZArith.vo theories/Arith/Wf_nat.vo @@ -12,7 +10,6 @@ contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/co contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo -contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Arith/Peano_dec.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo @@ -29,8 +26,7 @@ contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_ contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/PolyList.vo theories/Bool/Bool.vo theories/ZArith/ZArith.vo -contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v -contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith.vo theories/Arith/Minus.vo contrib/omega/OmegaSyntax.vo +contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith.vo theories/Arith/Minus.vo theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo @@ -136,7 +132,7 @@ theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo theories/Bool/Bool.vo: theories/Bool/Bool.v theories/Arith/Max.vo: theories/Arith/Max.v theories/Arith/Arith.vo theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo -theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo +theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/ArithSyntax.vo theories/Arith/Euclid.vo: theories/Arith/Euclid.v theories/Arith/Mult.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Peano_dec.vo: theories/Arith/Peano_dec.v theories/Logic/Decidable.vo theories/Arith/EqNat.vo: theories/Arith/EqNat.v @@ -152,6 +148,7 @@ theories/Arith/Le.vo: theories/Arith/Le.v theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo +theories/Arith/ArithSyntax.vo: theories/Arith/ArithSyntax.v theories/Logic/JMeq.vo: theories/Logic/JMeq.v theories/Logic/Decidable.vo: theories/Logic/Decidable.v theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v diff --git a/CHANGES b/CHANGES index f9ba8efbed..81d1a59e23 100644 --- a/CHANGES +++ b/CHANGES @@ -1,5 +1,39 @@ +Changes from V7.3 to ???? +------------------------- + +Language + +- Inductive definitions now accept ">" in constructor types to declare + the corresponding constructor as a coercion. + +ML tactic and vernacular commands + +- "Grammar tactic" and "Grammar vernac" of type "ast" are no longer + supported (only "Grammar tactic simple_tactic" of type "tactic" + remains available). +- Concrete syntax for ML written vernacular commands and tactics is + now declared at ML level using camlp4 macros TACTIC EXTEND et VERNAC + COMMAND EXTEND. + +Tactic definitions + +- static globalisation of identifiers and global references (source of + incompatibilities, especially, Recursive keyword is required for + mutually recursive definitions). + +Tactics + +- Double Induction now referring to hypotheses like "Intro until" +- "Inversion" now applies also on quantified hypotheses (naming as + for Intros until) +- NewDestruct now accepts terms with missing hypotheses + +Miscellaneous + +- Printing Coercion now used through the standard keywords Set/Add, Test, Print + Changes from V7.2 to V7.3 -========================= +------------------------- Language diff --git a/Makefile b/Makefile index b933ce3cc9..3282b3f915 100644 --- a/Makefile +++ b/Makefile @@ -54,7 +54,7 @@ DEPFLAGS=$(LOCALINCLUDES) OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS) OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS) -CAMLP4EXTENDFLAGS=-I . pa_extend.cmo q_MLast.cmo +CAMLP4EXTENDFLAGS=-I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p' COQINCLUDES= # coqtop includes itself the needed paths @@ -101,45 +101,62 @@ PRETYPING=pretyping/termops.cmo \ pretyping/coercion.cmo pretyping/cases.cmo pretyping/pretyping.cmo \ pretyping/syntax_def.cmo pretyping/pattern.cmo -PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ - parsing/termast.cmo parsing/astterm.cmo parsing/coqlib.cmo \ - parsing/g_prim.cmo parsing/g_basevernac.cmo \ +PARSING=parsing/lexer.cmo parsing/coqast.cmo \ + parsing/genarg.cmo proofs/tacexpr.cmo parsing/ast.cmo \ + parsing/termast.cmo parsing/astterm.cmo \ + parsing/extend.cmo parsing/esyntax.cmo \ + parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo \ + parsing/coqlib.cmo parsing/prettyp.cmo parsing/search.cmo + +HIGHPARSING= parsing/g_prim.cmo parsing/g_basevernac.cmo \ parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \ parsing/g_ltac.cmo parsing/g_constr.cmo parsing/g_cases.cmo \ - parsing/extend.cmo parsing/esyntax.cmo \ - parsing/printer.cmo parsing/prettyp.cmo parsing/search.cmo \ - parsing/egrammar.cmo \ - parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo + parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo PROOFS=proofs/proof_type.cmo proofs/proof_trees.cmo proofs/logic.cmo \ proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ proofs/clenv.cmo proofs/pfedit.cmo \ - proofs/tactic_debug.cmo proofs/tacinterp.cmo + proofs/tactic_debug.cmo TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ tactics/nbtermdn.cmo tactics/hipattern.cmo tactics/wcclausenv.cmo \ - tactics/tacticals.cmo tactics/tactics.cmo tactics/tacentries.cmo \ - tactics/hiddentac.cmo tactics/elim.cmo - -TOPLEVEL=toplevel/himsg.cmo toplevel/cerrors.cmo \ - toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \ - toplevel/record.cmo toplevel/recordobj.cmo \ - toplevel/discharge.cmo toplevel/vernacinterp.cmo toplevel/mltop.cmo \ - toplevel/vernac.cmo toplevel/vernacentries.cmo \ + tactics/tacticals.cmo tactics/tactics.cmo \ + tactics/hiddentac.cmo tactics/elim.cmo \ + tactics/dhyp.cmo tactics/auto.cmo tactics/tacinterp.cmo + +TOPLEVEL=toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \ + toplevel/command.cmo toplevel/record.cmo toplevel/recordobj.cmo \ + toplevel/discharge.cmo toplevel/vernacexpr.cmo \ + toplevel/vernacinterp.cmo toplevel/mltop.cmo \ + parsing/pcoq.cmo parsing/egrammar.cmo toplevel/metasyntax.cmo \ + toplevel/vernacentries.cmo toplevel/vernac.cmo \ toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \ toplevel/toplevel.cmo toplevel/usage.cmo \ toplevel/coqinit.cmo toplevel/coqtop.cmo -HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/setoid_replace.cmo\ - tactics/equality.cmo \ - tactics/inv.cmo tactics/leminv.cmo tactics/eauto.cmo \ - tactics/autorewrite.cmo tactics/refine.cmo tactics/eqdecide.cmo +HIGHTACTICS=tactics/setoid_replace.cmo tactics/equality.cmo \ + tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \ + tactics/autorewrite.cmo tactics/refine.cmo \ + tactics/extraargs.cmo tactics/extratactics.cmo tactics/eauto.cmo + +QUOTIFY=parsing/qast.cmo parsing/q_prim.cmo parsing/q_tactic.cmo + +parsing/q_prim.ml4: parsing/g_prim.ml4 + camlp4o -I parsing grammar.cma pa_ifdef.cmo pa_extend.cmo pr_o.cmo pr_extend.cmo -quotify -DQuotify -o parsing/q_prim.ml4 -impl parsing/g_prim.ml4 + +parsing/q_tactic.ml4: parsing/g_tactic.ml4 + camlp4o -I parsing grammar.cma pa_ifdef.cmo pa_extend.cmo pr_o.cmo pr_extend.cmo -quotify -DQuotify -o parsing/q_tactic.ml4 -impl parsing/g_tactic.ml4 -SPECTAC=tactics/tauto.ml4 +parsing/q_ltac.ml4: parsing/g_ltac.ml4 + camlp4o -I parsing grammar.cma pa_ifdef.cmo pa_extend.cmo pr_o.cmo pr_extend.cmo -quotify -DQuotify -o parsing/q_ltac.ml4 -impl parsing/g_ltac.ml4 + +SPECTAC= tactics/tauto.ml4 tactics/eqdecide.ml4 USERTAC = $(SPECTAC) -ML4FILES += $(USERTAC) +ML4FILES += $(USERTAC) tactics/extraargs.ml4 tactics/extratactics.ml4 \ + tactics/eauto.ml4 + USERTACCMO=$(USERTAC:.ml4=.cmo) USERTACCMX=$(USERTAC:.ml4=.cmx) @@ -153,11 +170,13 @@ INTERFACE=contrib/interface/vtp.cmo \ contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmo \ contrib/interface/blast.cmo contrib/interface/centaur.cmo +ML4FILES += contrib/interface/debug_tac.ml4 contrib/interface/centaur.ml4 + PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \ lib/util.cmo lib/dyn.cmo lib/gmap.cmo lib/gmapl.cmo \ lib/predicate.cmo lib/hashcons.cmo lib/profile.cmo \ lib/system.cmo lib/bstack.cmo lib/edit.cmo lib/options.cmo \ - lib/rtree.cmo \ + lib/rtree.cmo lib/gset.cmo lib/tlm.cmo \ kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo \ kernel/term.cmo kernel/sign.cmo kernel/declarations.cmo \ kernel/environ.cmo \ @@ -167,6 +186,7 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \ library/nameops.cmo library/libobject.cmo library/summary.cmo \ library/nametab.cmo library/lib.cmo library/global.cmo \ library/library.cmo lib/options.cmo library/impargs.cmo \ + library/goptions.cmo \ pretyping/evd.cmo pretyping/instantiate.cmo \ pretyping/termops.cmo \ pretyping/reductionops.cmo pretyping/retyping.cmo library/declare.cmo \ @@ -177,35 +197,53 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \ pretyping/coercion.cmo pretyping/inductiveops.cmo pretyping/cases.cmo \ pretyping/indrec.cmo \ pretyping/pretyping.cmo pretyping/syntax_def.cmo \ - parsing/lexer.cmo parsing/coqast.cmo \ + parsing/lexer.cmo parsing/coqast.cmo parsing/genarg.cmo \ + proofs/tacexpr.cmo toplevel/vernacexpr.cmo \ parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_prim.cmo parsing/g_basevernac.cmo \ - parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \ - parsing/g_ltac.cmo parsing/g_constr.cmo parsing/g_cases.cmo \ parsing/extend.cmo \ - parsing/coqlib.cmo library/goptions.cmo pretyping/detyping.cmo \ + parsing/coqlib.cmo pretyping/detyping.cmo \ parsing/termast.cmo parsing/astterm.cmo \ parsing/egrammar.cmo parsing/esyntax.cmo toplevel/metasyntax.cmo \ - parsing/printer.cmo pretyping/typing.cmo \ + parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo \ + lib/stamps.cmo pretyping/typing.cmo \ proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \ proofs/evar_refiner.cmo proofs/tacmach.cmo toplevel/himsg.cmo \ parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \ - toplevel/cerrors.cmo - -ML4FILES += contrib/correctness/psyntax.ml4 contrib/field/field.ml4 - -OMEGACMO=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo - -ROMEGACMO=contrib/romega/const_omega.cmo contrib/romega/refl_omega.cmo - -RINGCMO=contrib/ring/quote.cmo contrib/ring/ring.cmo + toplevel/class.cmo toplevel/recordobj.cmo toplevel/cerrors.cmo \ + parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \ + parsing/g_ltac.cmo parsing/g_constr.cmo parsing/g_cases.cmo \ + proofs/tactic_debug.cmo \ + proofs/pfedit.cmo proofs/clenv.cmo tactics/wcclausenv.cmo \ + tactics/tacticals.cmo tactics/hipattern.cmo \ + tactics/tactics.cmo tactics/hiddentac.cmo \ + tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ + tactics/nbtermdn.cmo tactics/dhyp.cmo tactics/elim.cmo \ + tactics/auto.cmo tactics/tacinterp.cmo tactics/extraargs.cmo \ + $(CMO) # Solution de facilité... + +ML4FILES += contrib/correctness/psyntax.ml4 contrib/omega/g_omega.ml4 \ + contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 \ + contrib/ring/g_ring.ml4 \ + contrib/field/field.ml4 contrib/fourier/g_fourier.ml4 \ + contrib/extraction/g_extraction.ml4 contrib/xml/xmlentries.ml4 + +OMEGACMO=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ + contrib/omega/g_omega.cmo + +ROMEGACMO=contrib/romega/const_omega.cmo contrib/romega/refl_omega.cmo \ + contrib/romega/g_romega.cmo + +RINGCMO=contrib/ring/quote.cmo contrib/ring/g_quote.cmo \ + contrib/ring/ring.cmo contrib/ring/g_ring.cmo FIELDCMO=contrib/field/field.cmo XMLCMO=contrib/xml/xml.cmo \ contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo -FOURIERCMO=contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo +FOURIERCMO=contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo \ + contrib/fourier/g_fourier.cmo EXTRACTIONCMO=contrib/extraction/table.cmo\ contrib/extraction/mlutil.cmo\ @@ -213,7 +251,8 @@ EXTRACTIONCMO=contrib/extraction/table.cmo\ contrib/extraction/haskell.cmo \ contrib/extraction/extraction.cmo \ contrib/extraction/common.cmo \ - contrib/extraction/extract_env.cmo + contrib/extraction/extract_env.cmo \ + contrib/extraction/g_extraction.cmo CORRECTNESSCMO=contrib/correctness/pmisc.cmo \ contrib/correctness/peffect.cmo contrib/correctness/prename.cmo \ @@ -230,6 +269,7 @@ JPROVERCMO=contrib/jprover/opname.cmo \ contrib/jprover/jtunify.cmo contrib/jprover/jall.cmo \ contrib/jprover/jprover.cmo +ML4FILES += contrib/jprover/jprover.ml4 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) $(XMLCMO) \ $(FOURIERCMO) \ @@ -238,8 +278,8 @@ CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) $(XMLCMO) \ CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) -CMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \ - $(PROOFS) $(TACTICS) $(TOPLEVEL) $(HIGHTACTICS) $(CONTRIB) +CMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) \ + $(PROOFS) $(TACTICS) $(PARSING) $(TOPLEVEL) $(HIGHPARSING) $(HIGHTACTICS) $(CONTRIB) CMX=$(CMO:.cmo=.cmx) ########################################################################### @@ -288,6 +328,7 @@ scripts/tolink.ml: Makefile echo "let proofs = \""$(PROOFS)"\"" >> $@ echo "let tactics = \""$(TACTICS)"\"" >> $@ echo "let toplevel = \""$(TOPLEVEL)"\"" >> $@ + echo "let highparsing = \""$(HIGHPARSING)"\"" >> $@ echo "let hightactics = \""$(HIGHTACTICS)" "$(USERTACCMO)"\"" >> $@ echo "let contrib = \""$(CONTRIB)"\"" >> $@ @@ -316,7 +357,9 @@ proofs: $(PROOFS) tactics: $(TACTICS) parsing: $(PARSING) pretyping: $(PRETYPING) +highparsing: $(HIGHPARSING) toplevel: $(TOPLEVEL) +hightactics: $(HIGHTACTICS) # special binaries for debugging @@ -344,7 +387,7 @@ check:: $(BESTCOQTOP) states:: states/barestate.coq states/initial.coq -SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v syntax/PPTactic.v +SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v states/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP) $(BESTCOQTOP) -boot -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq @@ -361,12 +404,9 @@ theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) init: $(INITVO) -EXTRACTIONVO=contrib/extraction/Extraction.vo +EXTRACTIONVO= -TACTICSVO=tactics/Equality.vo \ - tactics/Tauto.vo tactics/Inv.vo \ - tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo \ - tactics/EqDecide.vo tactics/Setoid_replace.vo $(EXTRACTIONVO) +TACTICSVO=$(EXTRACTIONVO) tactics/%.vo: tactics/%.v states/barestate.coq $(COQC) $(BOOTCOQTOP) -is states/barestate.coq -compile $* @@ -387,7 +427,8 @@ LOGICVO=theories/Logic/Hurkens.vo theories/Logic/ProofIrrelevance.vo\ theories/Logic/Berardi.vo theories/Logic/Eqdep_dec.vo \ theories/Logic/Decidable.vo theories/Logic/JMeq.vo -ARITHVO=theories/Arith/Arith.vo theories/Arith/Gt.vo \ +ARITHVO=theories/Arith/ArithSyntax.vo \ + theories/Arith/Arith.vo theories/Arith/Gt.vo \ theories/Arith/Between.vo theories/Arith/Le.vo \ theories/Arith/Compare.vo theories/Arith/Lt.vo \ theories/Arith/Compare_dec.vo theories/Arith/Min.vo \ @@ -516,7 +557,7 @@ CORRECTNESSVO=contrib/correctness/Arrays.vo \ contrib/correctness/Tuples.vo # contrib/correctness/ProgramsExtraction.vo -OMEGAVO = contrib/omega/Omega.vo contrib/omega/OmegaSyntax.vo +OMEGAVO = contrib/omega/Omega.vo ROMEGAVO = contrib/romega/ReflOmegaCore.vo contrib/romega/ROmega.vo @@ -529,13 +570,13 @@ RINGVO = contrib/ring/ArithRing.vo contrib/ring/Ring_normalize.vo \ FIELDVO = contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo \ contrib/field/Field_Tactic.vo contrib/field/Field.vo -XMLVO = contrib/xml/Xml.vo +XMLVO = Xml.vo INTERFACEV0 = contrib/interface/Centaur.vo contrib/interface/vernacrc FOURIERVO = contrib/fourier/Fourier_util.vo contrib/fourier/Fourier.vo -JPROVERVO = contrib/jprover/JProver.vo +JPROVERVO = contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE) $(BESTCOQTOP) -boot -byte $(COQINCLUDES) -compile $* @@ -544,9 +585,8 @@ contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/init $(BESTCOQTOP) -boot -byte $(COQINCLUDES) -compile $* CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ - $(CORRECTNESSVO)\ - $(INTERFACEV0) $(FOURIERVO) \ - $(JPROVERVO) + $(CORRECTNESSVO) $(FOURIERVO) \ + $(JPROVERVO) $(INTERFACEV0) $(CONTRIBVO): states/initial.coq @@ -706,9 +746,9 @@ LPLIB = lib/doc.tex $(LIBREP:.cmo=.mli) LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli) LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli) LPPRETYPING = pretyping/doc.tex pretyping/rawterm.mli $(PRETYPING:.cmo=.mli) -LPPARSING =$(PARSING:.cmo=.mli) +LPPARSING =$(PARSING:.cmo=.mli) $(HIGHPARSING:.cmo=.mli) LPPROOFS = proofs/doc.tex $(PROOFS:.cmo=.mli) -LPTACTICS = tactics/doc.tex $(TACTICS:.cmo=.mli) +LPTACTICS = tactics/doc.tex $(TACTICS:.cmo=.mli) $(HIGHTACTICS:.cmo=.mli) LPTOPLEVEL = toplevel/doc.tex $(TOPLEVEL:.cmo=.mli) LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) \ $(LPPRETYPING) $(LPPROOFS) $(LPTACTICS) $(LPTOPLEVEL) @@ -741,13 +781,22 @@ tags: # grammar modules with camlp4 -ML4FILES += parsing/lexer.ml4 parsing/q_coqast.ml4 \ +ML4FILES += parsing/lexer.ml4 parsing/q_util.ml4 parsing/q_coqast.ml4 \ parsing/g_prim.ml4 parsing/pcoq.ml4 -GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/dyn.cmo \ - lib/hashcons.cmo lib/predicate.cmo kernel/names.cmo \ - parsing/coqast.cmo parsing/lexer.cmo \ - parsing/pcoq.cmo parsing/q_coqast.cmo parsing/g_prim.cmo +CAMLP4EXTENSIONS= parsing/tacextend.cmo parsing/vernacextend.cmo + +GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \ + lib/dyn.cmo lib/options.cmo \ + lib/hashcons.cmo lib/predicate.cmo lib/rtree.cmo $(KERNEL) \ + library/summary.cmo library/nameops.cmo library/nametab.cmo \ + library/libobject.cmo library/lib.cmo library/global.cmo \ + library/goptions.cmo pretyping/rawterm.cmo pretyping/evd.cmo \ + parsing/coqast.cmo parsing/genarg.cmo \ + proofs/tacexpr.cmo proofs/proof_type.cmo parsing/ast.cmo \ + parsing/lexer.cmo parsing/q_util.cmo parsing/extend.cmo \ + toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_coqast.cmo \ + parsing/egrammar.cmo parsing/g_prim.cmo $(CAMLP4EXTENSIONS) parsing/grammar.cma: $(GRAMMARCMO) $(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ @@ -758,7 +807,7 @@ clean:: ML4FILES +=parsing/g_basevernac.ml4 parsing/g_minicoq.ml4 \ parsing/g_vernac.ml4 parsing/g_proofs.ml4 parsing/g_cases.ml4 \ parsing/g_constr.ml4 parsing/g_tactic.ml4 parsing/g_ltac.ml4 \ - parsing/extend.ml4 + parsing/tacextend.ml4 parsing/vernacextend.ml4 # beforedepend:: $(GRAMMARCMO) @@ -920,6 +969,9 @@ depend: beforedepend # 5. Finally, we erase the generated .ml files rm -f $(ML4FILESML) +ml4clean:: + rm -f $(ML4FILESML) + clean:: rm -f $(ML4FILESML) diff --git a/TODO b/TODO index 5dbac9958e..e53d95f8e0 100644 --- a/TODO +++ b/TODO @@ -1,10 +1,6 @@ -Distribution: - -- faire une passe sur les options de coqtop et coqc - Langage: -- Propager les contraintes arrière dans Cases (cf example doc/Cases.tex) +Distribution: Environnement: @@ -12,35 +8,41 @@ Environnement: Noyau: +Tactic: + +- Que contradiction raisonne a isomorphisme pres de False + Vernac: - Print / Print Proof en fait identiques ; Print ne devrait pas afficher les constantes opaques (devrait afficher qqchose comme ) Theories: + - Rendre transparent tous les theoremes prouvant {A}+{B} - Faire demarrer PolyList.nth a` l'indice 0 -Renommer l'actuel nth en nth1 ?? - -Grammaires: - -- revoir numarg/pure_numarg dans g_tactic.ml4 (regles a factoriser) + Renommer l'actuel nth en nth1 ?? Doc: - Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection -- Documenter le nouvel Assert x:=t. - Documenter le filtrage sur les types inductifs avec let-ins (dont la - compatibility V6) + compatibilite V6) - Ajouter let dans les règles du CIC -> FAIT, mais reste a documenter le let dans les inductifs et les champs manifestes dans les Record - revoir le chapitre sur les tactiques utilisateur - faut-il mieux spécifier la sémantique de Simpl (??) -- documenter @Definition and co -- Suggestions de la formation - Dans le Intros pattern on pourrait interpreter les _ - comme des hypotheses sur lesquelles on ferait Clear immediatement --> FAIT, semble-t'il +- Préciser la clarification syntaxique de IntroPattern +- preciser que Goal vient en dernier dans une clause pattern list et + qu'il doit apparaitre si il y a un "in" + +- Omega Time debranche mais Omega System et Omega Action remarchent ? +- Ajout "Replace in" (mais TODO) +- Syntaxe Conditional tac Rewrite marche, à documenter +- Documenter Dependent Rewrite et CutRewrite ? +- Ajouter les motifs sous-termes de ltac + + diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml index e6f6891f73..ffcb7c648e 100644 --- a/contrib/correctness/pcic.ml +++ b/contrib/correctness/pcic.ml @@ -52,7 +52,7 @@ let tuple_n n = (fun i -> let id = id_of_string ("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in - (false, (id, true, Ast.nvar (id_of_string ("T" ^ string_of_int i))))) + (false, Vernacexpr.AssumExpr (id, Ast.nvar (id_of_string ("T" ^ string_of_int i))))) l1n in let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index c7f1fc2ed7..d191b58ebf 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -220,6 +220,14 @@ let reduce_open_constr (em0,c) = let em = existential_map_of_constr c in (em,c) +let register id n = + let id' = match n with None -> id | Some id' -> id' in + Penv.register id id' + +let correctness_hook _ ref = + let pf_id = Nameops.basename (Nametab.sp_of_global (Global.env()) ref) in + register pf_id None + let correctness s p opttac = Pmisc.reset_names(); let p,oc,cty,v = coqast_of_prog p in @@ -228,14 +236,14 @@ let correctness s p opttac = let sigma = Evd.empty in let cty = Reduction.nf_betaiota cty in let id = id_of_string s in - start_proof id Declare.NeverDischarge sign cty; + start_proof id (false,Nametab.NeverDischarge) sign cty correctness_hook; Penv.new_edited id (v,p); if !debug then show_open_subgoals(); deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ()); let oc = reduce_open_constr oc in deb_mess (str"AFTER REDUCTION:" ++ fnl ()); deb_mess (Printer.prterm_env (Global.env()) (snd oc)); - let tac = (tclTHEN (Refine.refine_tac oc) automatic) in + let tac = (tclTHEN (Extratactics.refine_tac oc) automatic) in let tac = match opttac with | None -> tac | Some t -> tclTHEN tac t @@ -245,15 +253,11 @@ let correctness s p opttac = (* On redéfinit la commande "Save" pour enregistrer les nouveaux programmes *) - +(* open Vernacinterp let add = Vernacinterp.overwriting_vinterp_add -let register id n = - let id' = match n with None -> id | Some id' -> id' in - Penv.register id id' - let _ = let current_save = Vernacinterp.vinterp_map "SaveNamed" in add "SaveNamed" @@ -282,4 +286,4 @@ let _ = let pf_id = Pfedit.get_current_proof_name () in current_saveanonymous l (); register pf_id (Some id))) - +*) diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v deleted file mode 100644 index 0f69bce4a4..0000000000 --- a/contrib/extraction/Extraction.v +++ /dev/null @@ -1,86 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - [ (Extraction $c) ] -| extr_list [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] -> - [ (ExtractionRec ($LIST $l)) ] - -(* Monolithic extraction to a file *) -| extr_file - [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] - -> [ (ExtractionFile $f ($LIST $l)) ] - -(* Modular extraction (one Coq module = one ML module) *) -| extr_module - [ "Extraction" "Module" identarg($m) "." ] - -> [ (ExtractionModule $m) ] -| rec_extr_module - [ "Recursive" "Extraction" "Module" identarg($m) "." ] - -> [ (RecursiveExtractionModule $m) ] - -(* Target Language *) - -| extr_language - [ "Extraction" "Language" extraction_language($l) "." ] - -> [ (ExtractionLang $l) ] - -(* Custom inlining directives *) -| inline_constant - [ "Extraction" "Inline" ne_qualidarg_list($l) "." ] - -> [ (ExtractionInline ($LIST $l)) ] - -| no_inline_constant - [ "Extraction" "NoInline" ne_qualidarg_list($l) "." ] - -> [ (ExtractionNoInline ($LIST $l)) ] - -| print_inline_constant - [ "Print" "Extraction" "Inline" "."] - -> [ (PrintExtractionInline) ] - -| reset_inline_constant - [ "Reset" "Extraction" "Inline" "."] - -> [ (ResetExtractionInline) ] - -(* Overriding of a Coq object by an ML one *) -| extract_constant - [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ] - -> [ (ExtractConstant $x $y) ] - -| extract_inlined_constant - [ "Extract" "Inlined" "Constant" qualidarg($x) - "=>" idorstring($y) "." ] - -> [ (ExtractInlinedConstant $x $y) ] - -| extract_inductive - [ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."] - -> [ (ExtractInductive $x $y) ] - -(* Utility entries *) -with mindnames : ast := - mlconstr [ idorstring($id) "[" idorstring_list($idl) "]" ] - -> [(VERNACARGLIST $id ($LIST $idl))] - -with idorstring_list: ast list := - ids_nil [ ] -> [ ] -| ids_cons [ idorstring($x) idorstring_list($l) ] -> [ $x ($LIST $l) ] - -with idorstring : ast := - ids_ident [ identarg($id) ] -> [ $id ] -| ids_string [ stringarg($s) ] -> [ $s ] - -with extraction_language : ast := - ocaml [ "Ocaml" ] -> [ "Ocaml" ] -| haskell [ "Haskell" ] -> [ "Haskell" ] -| toplevel [ "Toplevel" ] -> [ "Toplevel" ] - -. - diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index ecfd5e2ea8..db2e7d4f93 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -241,40 +241,33 @@ let extract_reference r = else List.find (decl_in_r r) decls in msgnl (pp_decl d) -let _ = - vinterp_add "Extraction" - (function - | [VARG_CONSTR ast] -> - (fun () -> - set_globals (); - let c = Astterm.interp_constr Evd.empty (Global.env()) ast in - match kind_of_term c with - (* If it is a global reference, then output the declaration *) - | Const sp -> extract_reference (ConstRef sp) - | Ind ind -> extract_reference (IndRef ind) - | Construct cs -> extract_reference (ConstructRef cs) - (* Otherwise, output the ML type or expression *) - | _ -> - match extract_constr (Global.env()) c with - | Emltype (t,_,_) -> msgnl (pp_type t ++ fnl ()) - | Emlterm a -> msgnl (pp_ast (normalize a) ++ fnl ())) - | _ -> assert false) +let extraction rawconstr = + set_globals (); + let c = Astterm.interp_constr Evd.empty (Global.env()) rawconstr in + match kind_of_term c with + (* If it is a global reference, then output the declaration *) + | Const sp -> extract_reference (ConstRef sp) + | Ind ind -> extract_reference (IndRef ind) + | Construct cs -> extract_reference (ConstructRef cs) + (* Otherwise, output the ML type or expression *) + | _ -> + match extract_constr (Global.env()) c with + | Emltype (t,_,_) -> msgnl (pp_type t ++ fnl ()) + | Emlterm a -> msgnl (pp_ast (normalize a) ++ fnl ()) (*s Recursive extraction in the Coq toplevel. The vernacular command is \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env] to get the saturated environment to extract. *) let mono_extraction (f,m) vl = - let refs = refs_of_vargl vl in + let refs = List.map Nametab.global vl in let prm = {modular=false; mod_name = m; to_appear= refs} in let decls = decl_of_refs refs in let decls = add_ml_decls prm decls in let decls = optimize prm decls in extract_to_file f prm decls -let _ = - vinterp_add "ExtractionRec" - (fun vl () -> mono_extraction (None,id_of_string "Main") vl) +let extraction_rec = mono_extraction (None,id_of_string "Main") (*s Extraction to a file (necessarily recursive). The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn]. @@ -297,14 +290,9 @@ let lang_error () = ++ fnl () ++ str "You should use Extraction Language Ocaml or Haskell before.") -let _ = - vinterp_add "ExtractionFile" - (function - | VARG_STRING f :: vl -> - (fun () -> - if lang () = Toplevel then lang_error () - else mono_extraction (filename f) vl) - | _ -> assert false) +let extraction_file f vl = + if lang () = Toplevel then lang_error () + else mono_extraction (filename f) vl (*s Extraction of a module. The vernacular command is \verb!Extraction Module! [M]. *) @@ -322,48 +310,37 @@ let module_file_name m = match lang () with | Haskell -> (String.capitalize (string_of_id m)) ^ ".hs" | Toplevel -> assert false -let _ = - vinterp_add "ExtractionModule" - (function - | [VARG_IDENTIFIER m] -> - (fun () -> - if lang () = Toplevel then lang_error () - else - let dir_m = module_of_id m in - let f = module_file_name m in - let prm = {modular=true; mod_name=m; to_appear=[]} in - let rl = extract_module dir_m in - let decls = optimize prm (decl_of_refs rl) in - let decls = add_ml_decls prm decls in - check_one_module dir_m decls; - let decls = List.filter (decl_in_m dir_m) decls in - extract_to_file (Some f) prm decls) - | _ -> assert false) +let extraction_module m = + if lang () = Toplevel then lang_error () + else + let dir_m = module_of_id m in + let f = module_file_name m in + let prm = {modular=true; mod_name=m; to_appear=[]} in + let rl = extract_module dir_m in + let decls = optimize prm (decl_of_refs rl) in + let decls = add_ml_decls prm decls in + check_one_module dir_m decls; + let decls = List.filter (decl_in_m dir_m) decls in + extract_to_file (Some f) prm decls (*s Recursive Extraction of all the modules [M] depends on. The vernacular command is \verb!Recursive Extraction Module! [M]. *) -let _ = - vinterp_add "RecursiveExtractionModule" - (function - | [VARG_IDENTIFIER m] -> - (fun () -> - if lang () = Toplevel then lang_error () - else - let dir_m = module_of_id m in - let modules,refs = - modules_extract_env dir_m in - check_modules modules; - let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in - let decls = optimize dummy_prm (decl_of_refs refs) in - let decls = add_ml_decls dummy_prm decls in - Dirset.iter - (fun m -> - let short_m = snd (split_dirpath m) in - let f = module_file_name short_m in - let prm = {modular=true;mod_name=short_m;to_appear=[]} in - let decls = List.filter (decl_in_m m) decls in - if decls <> [] then extract_to_file (Some f) prm decls) - modules) - | _ -> assert false) - +let recursive_extraction_module m = + if lang () = Toplevel then lang_error () + else + let dir_m = module_of_id m in + let modules,refs = + modules_extract_env dir_m in + check_modules modules; + let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in + let decls = optimize dummy_prm (decl_of_refs refs) in + let decls = add_ml_decls dummy_prm decls in + Dirset.iter + (fun m -> + let short_m = snd (split_dirpath m) in + let f = module_file_name short_m in + let prm = {modular=true;mod_name=short_m;to_appear=[]} in + let decls = List.filter (decl_in_m m) decls in + if decls <> [] then extract_to_file (Some f) prm decls) + modules diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli index 710e801d12..1cdb5c02c3 100644 --- a/contrib/extraction/extract_env.mli +++ b/contrib/extraction/extract_env.mli @@ -10,3 +10,12 @@ (*s This module declares the extraction commands. *) +open Util +open Names +open Nametab + +val extraction : Genarg.constr_ast -> unit +val extraction_rec : qualid located list -> unit +val extraction_file : string -> qualid located list -> unit +val extraction_module : identifier -> unit +val recursive_extraction_module : identifier -> unit diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 896203486b..ee7267f3f6 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -13,6 +13,7 @@ open Lib open Libobject open Goptions open Vernacinterp +open Extend open Names open Util open Pp @@ -66,21 +67,25 @@ let check_constant r = else errorlabstrm "extract_constant" (Printer.pr_global r ++ spc () ++ str "is not a constant.") +(* let string_of_varg = function | VARG_IDENTIFIER id -> string_of_id id | VARG_STRING s -> s | _ -> assert false +*) let no_such_reference q = errorlabstrm "reference_of_varg" (str "There is no such reference " ++ Nametab.pr_qualid q ++ str ".") +(* let reference_of_varg = function | VARG_QUALID q -> (try Nametab.locate q with Not_found -> no_such_reference q) | _ -> assert false let refs_of_vargl = List.map reference_of_varg +*) (*s Target Language *) @@ -103,18 +108,7 @@ let _ = declare_summary "Extraction Lang" init_function = (fun () -> lang_ref := Ocaml); survive_section = true } -let lang_to_lang = function - "Ocaml" -> Ocaml - | "Haskell" -> Haskell - | "Toplevel" -> Toplevel - | _ -> assert false - -let _ = - vinterp_add "ExtractionLang" - (function - [VARG_STRING l] -> - (fun () -> add_anonymous_leaf (extr_lang (lang_to_lang l))) - | _ -> assert false) +let extraction_language x = add_anonymous_leaf (extr_lang x) (*s Table for custom inlining *) @@ -150,21 +144,13 @@ let _ = declare_summary "Extraction Inline" (*s Grammar entries. *) -let _ = - vinterp_add "ExtractionInline" - (fun vl () -> - let refs = List.map check_constant (refs_of_vargl vl) in - add_anonymous_leaf (inline_extraction (true,refs))) - -let _ = - vinterp_add "ExtractionNoInline" - (fun vl () -> - let refs = List.map check_constant (refs_of_vargl vl) in - add_anonymous_leaf (inline_extraction (false,refs))) +let extraction_inline b vl = + let refs = List.map (fun x -> check_constant (Nametab.global x)) vl in + add_anonymous_leaf (inline_extraction (true,refs)) (*s Printing part *) -let print_inline () = +let print_extraction_inline () = let (i,n)= !inline_table in let i'= Refset.filter is_constant i in msg @@ -177,9 +163,6 @@ let print_inline () = (fun r p -> (p ++ str " " ++ Printer.pr_global r ++ fnl ())) n (mt ())) -let _ = vinterp_add "PrintExtractionInline" (fun _ -> print_inline) - - (*s Reset part *) let (reset_inline,_) = @@ -189,10 +172,8 @@ let (reset_inline,_) = load_function = (fun (_,_)-> inline_table := empty_inline_table); open_function = (fun _ -> ()); export_function = (fun x -> Some x) }) - -let _ = vinterp_add "ResetExtractionInline" - (fun _ () -> add_anonymous_leaf (reset_inline ())) - + +let reset_extraction_inline () = add_anonymous_leaf (reset_inline ()) (*s Table for direct ML extractions. *) @@ -235,30 +216,13 @@ let _ = declare_summary "ML extractions" (*s Grammar entries. *) -let _ = - vinterp_add "ExtractConstant" - (function - | [id; vs] -> - (fun () -> - let r = check_constant (reference_of_varg id) in - let s = string_of_varg vs in - add_anonymous_leaf (inline_extraction (false,[r])); - add_anonymous_leaf (in_ml_extraction (r,s))) - | _ -> assert false) - -let _ = - vinterp_add "ExtractInlinedConstant" - (function - | [id; vs] -> - (fun () -> - let r = check_constant (reference_of_varg id) in - let s = string_of_varg vs in - add_anonymous_leaf (inline_extraction (true,[r])); - add_anonymous_leaf (in_ml_extraction (r,s))) - | _ -> assert false) - - -let extract_inductive r (id2,l2) = match r with +let extract_constant_inline inline qid s = + let r = check_constant (Nametab.global qid) in + add_anonymous_leaf (inline_extraction (inline,[r])); + add_anonymous_leaf (in_ml_extraction (r,s)) + +let extract_inductive r (id2,l2) = + let r = Nametab.global r in match r with | IndRef ((sp,i) as ip) -> let mib = Global.lookup_mind sp in let n = Array.length mib.mind_packets.(i).mind_consnames in @@ -273,13 +237,3 @@ let extract_inductive r (id2,l2) = match r with | _ -> errorlabstrm "extract_inductive" (Printer.pr_global r ++ spc () ++ str "is not an inductive type.") - -let _ = - vinterp_add "ExtractInductive" - (function - | [q1; VARG_VARGLIST (id2 :: l2)] -> - (fun () -> - extract_inductive (reference_of_varg q1) - (string_of_varg id2, List.map string_of_varg l2)) - | _ -> assert false) - diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index a6cde3c5f2..9fa7142ce8 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -28,7 +28,7 @@ module Refset : Set.S with type elt = global_reference val check_constant : global_reference -> global_reference -val refs_of_vargl : vernac_arg list -> global_reference list +(*val refs_of_vargl : Extend.vernac_arg list -> global_reference list*) (*s Target language. *) @@ -52,3 +52,18 @@ val ml_extractions : unit -> Refset.t val sorted_ml_extractions : unit -> (global_reference * string) list +(*s Extraction commands. *) + +open Util + +val extraction_language : lang -> unit + +val extraction_inline : bool -> qualid located list -> unit + +val print_extraction_inline : unit -> unit + +val reset_extraction_inline : unit -> unit + +val extract_constant_inline : bool -> qualid located -> string -> unit + +val extract_inductive : qualid located -> string * string list -> unit diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 74a58b11d4..c877dc47bb 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -18,8 +18,10 @@ open Term open Tactics open Clenv open Names +open Tacticals open Tacmach open Fourier +open Contradiction (****************************************************************************** Opérations sur les combinaisons linéaires affines. @@ -68,6 +70,7 @@ let flin_emult a f = ;; (*****************************************************************************) +open Vernacexpr let parse_ast = Pcoq.parse_string Pcoq.Constr.constr;; let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);; let pf_parse_constr gl s = @@ -550,10 +553,11 @@ let rec fourier gl= ;; +(* let fourier_tac x gl = fourier gl ;; let v_fourier = add_tactic "Fourier" fourier_tac - +*) diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 6df04bd37d..a8b9651148 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -28,6 +28,7 @@ open Declarations open Environ open Sign open Inductive +open Tacticals open Tacmach open Evar_refiner open Tactics @@ -35,6 +36,7 @@ open Clenv open Logic open Nametab open Omega +open Contradiction (* Added by JCF, 09/03/98 *) @@ -48,6 +50,46 @@ let display_system_flag = ref false let display_action_flag = ref false let old_style_flag = ref false +let read f () = !f +let write f x = f:=x + +open Goptions + +(* Obsolete, subsumed by Time Omega +let _ = + declare_bool_option + { optsync = false; + optname = "Omega time displaying flag"; + optkey = SecondaryTable ("Omega","Time"); + optread = read display_time_flag; + optwrite = write display_time_flag } +*) + +let _ = + declare_bool_option + { optsync = false; + optname = "Omega system time displaying flag"; + optkey = SecondaryTable ("Omega","System"); + optread = read display_system_flag; + optwrite = write display_system_flag } + +let _ = + declare_bool_option + { optsync = false; + optname = "Omega action display flag"; + optkey = SecondaryTable ("Omega","Action"); + optread = read display_action_flag; + optwrite = write display_action_flag } + +let _ = + declare_bool_option + { optsync = false; + optname = "Omega old style flag"; + optkey = SecondaryTable ("Omega","OldStyle"); + optread = read old_style_flag; + optwrite = write old_style_flag } + + let all_time = timing "Omega " let solver_time = timing "Solver " let exact_time = timing "Rewrites " @@ -70,7 +112,8 @@ let new_identifier_var = let rec mk_then = function [t] -> t | (t::l) -> (tclTHEN (t) (mk_then l)) | [] -> tclIDTAC -let exists_tac c = constructor_tac (Some 1) 1 [Com,c] +let exists_tac c = constructor_tac (Some 1) 1 (Rawterm.ImplicitBindings [c]) + let generalize_tac t = generalize_time (generalize t) let elim t = elim_time (simplest_elim t) let exact t = exact_time (Tactics.refine t) @@ -1822,7 +1865,3 @@ let omega_solver gl = (* if !display_time_flag then begin text_time (); flush Pervasives.stdout end; *) result - -let omega = hide_atomic_tactic "Omega" omega_solver - - diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 669fd21c50..bcd8ee5f94 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -112,7 +112,7 @@ open Pattern open Tacmach open Tactics open Proof_trees -open Proof_type +open Tacexpr (*i*) (*s First, we need to access some Coq constants @@ -452,18 +452,6 @@ let quote f lid gl = | None -> Tactics.convert_concl (mkApp (f, [| p |])) gl | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) gl -(*i*) -let dyn_quote = function - | [Identifier f] -> quote f [] - | Identifier f :: lid -> quote f - (List.map (function - | Identifier id -> id - | other -> bad_tactic_args "Quote" [other]) lid) - | l -> bad_tactic_args "Quote" l - -let h_quote = hide_tactic "Quote" dyn_quote -(*i*) - (*i Just testing ... diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index e6635c441b..25c3f74917 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -17,12 +17,14 @@ open Term open Names open Nameops open Reductionops +open Tacticals +open Tacexpr open Tacmach -open Proof_type open Proof_trees open Printer open Equality open Vernacinterp +open Vernacexpr open Libobject open Closure open Tacred @@ -227,34 +229,34 @@ let unbox = function (* Add a Ring or a Semi-Ring to the database after a type verification *) +let implement_theory env t th args = + is_conv env Evd.empty (Typing.type_of env Evd.empty t) (mkLApp (th, args)) + let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset = if theories_map_mem a then errorlabstrm "Add Semi Ring" (str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++ prterm a); let env = Global.env () in if (want_ring & want_setoid & - (not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (mkLApp (coq_Setoid_Ring_Theory, - [| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])))) & - (not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth)) - (mkLApp (coq_Setoid_Theory, [| a; (unbox aequiv) |]))))) then + not (implement_theory env t coq_Setoid_Ring_Theory + [| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|]) + & + not (implement_theory env (unbox asetth) coq_Setoid_Theory + [| a; (unbox aequiv) |])) then errorlabstrm "addring" (str "Not a valid Setoid-Ring theory"); if (not want_ring & want_setoid & - (not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (mkLApp (coq_Semi_Setoid_Ring_Theory, - [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|])))) & - (not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth)) - (mkLApp (coq_Setoid_Theory, [| a; (unbox aequiv) |]))))) then + not (implement_theory env t coq_Semi_Setoid_Ring_Theory + [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) & + not (implement_theory env (unbox asetth) coq_Setoid_Theory + [| a; (unbox aequiv) |])) then errorlabstrm "addring" (str "Not a valid Semi-Setoid-Ring theory"); if (want_ring & not want_setoid & - not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (mkLApp (coq_Ring_Theory, - [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])))) then + not (implement_theory env t coq_Ring_Theory + [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])) then errorlabstrm "addring" (str "Not a valid Ring theory"); if (not want_ring & not want_setoid & - not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (mkLApp (coq_Semi_Ring_Theory, - [| a; aplus; amult; aone; azero; aeq |])))) then + not (implement_theory env t coq_Semi_Ring_Theory + [| a; aplus; amult; aone; azero; aeq |])) then errorlabstrm "addring" (str "Not a valid Semi-Ring theory"); Lib.add_anonymous_leaf (theory_to_obj @@ -274,151 +276,6 @@ let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus th_t = t; th_closed = cset })) -(* The vernac commands "Add Ring" and "Add Semi Ring" *) -(* see file Ring.v for examples of this command *) - -let constr_of_comarg = function - | VARG_CONSTR c -> constr_of c - | _ -> anomaly "Add (Semi) (Setoid) Ring" - -let cset_of_comarg_list l = - List.fold_right ConstrSet.add (List.map constr_of_comarg l) ConstrSet.empty - -let _ = - vinterp_add "AddSemiRing" - (function - | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult) - ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aeq) - ::(VARG_CONSTR t)::l -> - (fun () -> (add_theory false false false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - (cset_of_comarg_list l))) - | _ -> anomaly "AddSemiRing") - -let _ = - vinterp_add "AddRing" - (function - | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult) - ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp) - ::(VARG_CONSTR aeq)::(VARG_CONSTR t)::l -> - (fun () -> (add_theory true false false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - (cset_of_comarg_list l))) - | _ -> anomaly "AddRing") - -let _ = - vinterp_add "AddSetoidRing" - (function - | (VARG_CONSTR a)::(VARG_CONSTR aequiv)::(VARG_CONSTR asetth)::(VARG_CONSTR aplus) - ::(VARG_CONSTR amult)::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp) - ::(VARG_CONSTR aeq)::(VARG_CONSTR pm)::(VARG_CONSTR mm)::(VARG_CONSTR om) - ::(VARG_CONSTR t)::l -> - (fun () -> (add_theory true false true - (constr_of a) - (Some (constr_of aequiv)) - (Some (constr_of asetth)) - (Some { - plusm = (constr_of pm); - multm = (constr_of mm); - oppm = Some (constr_of om)}) - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - (cset_of_comarg_list l))) - | _ -> anomaly "AddSetoidRing") - -let _ = - vinterp_add "AddSemiSetoidRing" - (function - | (VARG_CONSTR a)::(VARG_CONSTR aequiv)::(VARG_CONSTR asetth)::(VARG_CONSTR aplus) - ::(VARG_CONSTR amult)::(VARG_CONSTR aone)::(VARG_CONSTR azero) - ::(VARG_CONSTR aeq)::(VARG_CONSTR pm)::(VARG_CONSTR mm) - ::(VARG_CONSTR t)::l -> - (fun () -> (add_theory false false true - (constr_of a) - (Some (constr_of aequiv)) - (Some (constr_of asetth)) - (Some { - plusm = (constr_of pm); - multm = (constr_of mm); - oppm = None}) - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - (cset_of_comarg_list l))) - | _ -> anomaly "AddSemiSetoidRing") - -let _ = - vinterp_add "AddAbstractSemiRing" - (function - | [VARG_CONSTR a; VARG_CONSTR aplus; - VARG_CONSTR amult; VARG_CONSTR aone; - VARG_CONSTR azero; VARG_CONSTR aeq; VARG_CONSTR t] -> - (fun () -> (add_theory false true false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - ConstrSet.empty)) - | _ -> anomaly "AddAbstractSemiRing") - -let _ = - vinterp_add "AddAbstractRing" - (function - | [ VARG_CONSTR a; VARG_CONSTR aplus; - VARG_CONSTR amult; VARG_CONSTR aone; - VARG_CONSTR azero; VARG_CONSTR aopp; - VARG_CONSTR aeq; VARG_CONSTR t ] -> - (fun () -> (add_theory true true false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - ConstrSet.empty)) - | _ -> anomaly "AddAbstractRing") - (******** The tactic itself *********) (* @@ -894,14 +751,13 @@ let guess_eq_tac th = (tclTHEN (* Normalized sums associate on the right *) (tclREPEAT - (tclTHENST + (tclTHENFIRST (apply (mkApp(build_coq_f_equal2 (), [| th.th_a; th.th_a; th.th_a; th.th_plus |]))) - [reflexivity] - tclIDTAC)) + reflexivity)) (tclTRY - (tclTHENL + (tclTHENLAST (apply (mkApp(build_coq_f_equal2 (), [| th.th_a; th.th_a; th.th_a; th.th_plus |]))) @@ -964,13 +820,3 @@ let polynom lc gl = errorlabstrm "Ring :" (str" All terms must have the same type"); (tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl - -let dyn_polynom ltacargs gl = - polynom (List.map - (function - | Command c -> pf_interp_constr gl c - | Constr c -> c - | _ -> anomaly "dyn_polynom") - ltacargs) gl - -let v_polynom = add_tactic "Ring" dyn_polynom diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index 9ff41f0b52..788d3338cf 100644 --- a/contrib/romega/refl_omega.ml +++ b/contrib/romega/refl_omega.ml @@ -596,7 +596,9 @@ let coq_omega gl = with Omega.NO_CONTRADICTION -> Util.error "Omega can't solve this system" end +(* let refl_omega = Tacmach.hide_atomic_tactic "StepOmega" coq_omega +*) (* \section{Encapsulation ROMEGA} *) @@ -614,6 +616,7 @@ open Term open Environ open Sign open Inductive +open Tacticals open Tacmach open Tactics open Tacticals @@ -832,5 +835,7 @@ let omega_solver gl = in (loop concl) gl +(* let omega = hide_atomic_tactic "ReflOmega" omega_solver +*) diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli index 6d8250ef76..07335ea6a5 100644 --- a/contrib/xml/xmlcommand.mli +++ b/contrib/xml/xmlcommand.mli @@ -28,7 +28,7 @@ (* Note: it is printed only (and directly) the most cooked available *) (* form of the definition (all the parameters are *) (* lambda-abstracted, but the object can still refer to variables) *) -val print : Nametab.qualid -> string option -> unit +val print : Nametab.qualid Util.located -> string option -> unit (* show dest *) (* where dest is either None (for stdout) or (Some filename) *) @@ -46,7 +46,7 @@ val printAll : unit -> unit (* and terms of the module d *) (* Note: the terms are printed in their uncooked form plus the informations *) (* on the parameters of their most cooked form *) -val printModule : Nametab.qualid -> string option -> unit +val printModule : Nametab.qualid Util.located -> string option -> unit (* printSection identifier directory_name *) (* where identifier is the name of a closed section d *) diff --git a/dev/changements.txt b/dev/changements.txt index 29eab892e8..a294082f75 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -1,3 +1,45 @@ +MAIN CHANGES FROM COQ V7.3 +========================== + +New parsing model for tactics and vernacular commands + + - Introduction of a dedicated type for tactic expressions + (Tacexpr.raw_tactic_expr) + - Introduction of a dedicated type for vernac expressions + (Vernacexpr.vernac_expr) + - Declaration of new vernacular parsing rules by a new camlp4 macro + GRAMMAR COMMAND EXTEND ... END to be used in ML files + - Declaration of new tactics parsing/printing rules by a new camlp4 macro + TACTIC EXTEND ... END to be used in ML files + +New organisation of THENS: +tclTHENS tac tacs : tacs is now an array +tclTHENSFIRSTn tac1 tacs tac2 : + apply tac1 then, apply the array tacs on the first n subgoals and + tac2 on the remaining subgoals (previously tclTHENST) +tclTHENSLASTn tac1 tac2 tacs : + apply tac1 then, apply tac2 on the first subgoals and apply the array + tacs on the last n subgoals +tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI) +tclTHENLASTn tac1 tacs = tclTHENSLASTn tac1 tclIDTAC tacs +tclTHENFIRST tac1 tac2 = tclTHENFIRSTn tac1 [|tac2|] +tclTHENLAST tac1 tac2 = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL) +tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number") +tclTHENSV same as tclTHENS but with an array +tclTHENSi : no longer available + +Proof_type: subproof field in type proof_tree glued with the ref field + +Tacmach: no more echo from functions of module Refiner + +Files contrib/*/g_*.ml4 take the place of files contrib/*/*.v. +Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd + VERNAC COMMAND EXTEND macros +File syntax/PPTactic.v moved to parsing/pptactic.ml +Tactics about False and not now in tactics/contradiction.ml +Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v) +File tacinterp.ml moved from proofs to directory tactics + MAIN CHANGES FROM COQ V7.1 TO COQ V7.2 ====================================== diff --git a/dev/db_printers.ml b/dev/db_printers.ml index c7857e968f..3e4ba263f9 100644 --- a/dev/db_printers.ml +++ b/dev/db_printers.ml @@ -8,7 +8,7 @@ open Pp open Names -let pP s = pP (hov 0 s) +let pp s = pp (hov 0 s) let prid id = Format.print_string (string_of_id id) let prsp sp = Format.print_string (string_of_path sp) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b179428845..417bbfce2b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -79,7 +79,7 @@ let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]") let ppenv e = pp (pr_rel_context e (rel_context e)) -let pptac = (fun x -> pp(gentacpr x)) +let pptac = (fun x -> pp(Pptactic.pr_raw_tactic x)) let cnt = ref 0 diff --git a/doc/newsyntax.tex b/doc/newsyntax.tex index eb005520d3..035d3d8bd2 100644 --- a/doc/newsyntax.tex +++ b/doc/newsyntax.tex @@ -676,4 +676,10 @@ Remplacer Save. par Qed. Remplacer Implicit Arguments On/Off par Set/Unset Implicit Arguments. +La syntaxe \verb=Intros (a,b)= est inutile, \verb=Intros [a b]= fait l'affaire. + +Mettre des \verb=?x= plutot que des \verb=?1= dans les motifs de ltac ?? + +Virer \verb=Goal= sans argument (synonyme de \verb=Proof= et sans effets). + \end{document} diff --git a/parsing/extend.ml4 b/parsing/extend.ml4 deleted file mode 100644 index e54ac11bba..0000000000 --- a/parsing/extend.ml4 +++ /dev/null @@ -1,303 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* not (Lexer.is_keyword s) - | _ -> false - -let is_number s = - match s.[0] with - | '0'..'9' -> true - | _ -> false - -let strip s = - let len = - let rec loop i len = - if i = String.length s then len - else if s.[i] == ' ' then loop (i + 1) len - else loop (i + 1) (len + 1) - in - loop 0 0 - in - if len == String.length s then s - else - let s' = String.create len in - let rec loop i i' = - if i == String.length s then s' - else if s.[i] == ' ' then loop (i + 1) i' - else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end - in - loop 0 0 - -let terminal s = - let s = strip s in - if s = "" then failwith "empty token"; - if is_ident_not_keyword s then ("IDENT", s) - else if is_number s then ("INT", s) - else ("", s) - - - -let qualified_nterm current_univ ntrm = - match ntrm with - NtQual (univ, en) -> (get_univ univ, en) - | NtShort en -> (current_univ, en) - -(* For compatibility *) -let rename_command nt = - if String.length nt >= 7 & String.sub nt 0 7 = "command" - then "constr"^(String.sub nt 7 (String.length nt - 7)) - else if nt = "lcommand" then "lconstr" - else if nt = "lassoc_command4" then "lassoc_constr4" - else nt - -let nterm univ ast = - - let nont = - match ast with - | Node (_, "QUAL", [Id (_, u); Id (_, nt)]) -> - NtQual (rename_command u, rename_command nt) - | Id (_, nt) -> NtShort (rename_command nt) - | _ -> invalid_arg_loc (Ast.loc ast, "Extend.nterm") - in - let (u,n) = qualified_nterm univ nont in - let e = - try - get_entry u n - with UserError _ -> - user_err_loc(loc ast,"Externd.nterm", str"unknown grammar entry") - in - (nont, type_of_entry e) - -let prod_item univ env ast = - match ast with - | Str (_, s) -> env, Term (terminal s) - | Node (_, "NT", [nt; Nmeta (locp, p)]) -> - let (nont, etyp) = nterm univ nt in - ((p, etyp) :: env, NonTerm (nont, etyp, Some p)) - | Node (_, "NT", [nt]) -> - let (nont, etyp) = nterm univ nt in - env, NonTerm (nont, etyp, None) - | _ -> invalid_arg_loc (Ast.loc ast, "Extend.prod_item") - -let rec prod_item_list univ penv pil = - match pil with - | [] -> [], penv - | pi :: pitl -> - let (env, pic) = prod_item univ penv pi in - let (pictl, act_env) = prod_item_list univ env pitl in - (pic :: pictl, act_env) - -let gram_rule univ etyp ast = - match ast with - | Node (_, "GRAMMARRULE", (Id (_, name) :: act :: pil)) -> - let (pilc, act_env) = prod_item_list univ [] pil in - let a = Ast.to_act_check_vars act_env etyp act in - { gr_name=name; gr_production=pilc; gr_action=a } - | _ -> invalid_arg_loc (Ast.loc ast, "Extend.gram_rule") - -let gram_entry univ (nt, etyp, ass, rl) = - { ge_name = nt; - ge_type = etyp; - gl_assoc = ass; - gl_rules = List.map (gram_rule univ etyp) rl } - -let gram_assoc = function - | Node (_, "LEFTA", []) -> Some LeftA - | Node (_, "RIGHTA", []) -> Some RightA - | Node (_, "NONA", []) -> Some NonA - | Node (_, "NONE", []) -> None - | ast -> invalid_arg_loc (Ast.loc ast, "Egrammar.assoc") - -let gram_define_entry univ = function - | Node (_, "GRAMMARENTRY", (Id (ntl, nt) :: et :: ass :: rl)) -> - let etyp = entry_type et in - let assoc = gram_assoc ass in - - (* For compatibility *) - let nt = rename_command nt in - - let _ = - try - create_entry univ nt etyp - with Failure s -> - user_err_loc (ntl,"gram_define_entry", str s) - in - (nt, etyp, assoc, rl) - | ast -> invalid_arg_loc (Ast.loc ast, "gram_define_entry") - -let interp_grammar_command univ astl = - - (* For compatibility *) - let univ = rename_command univ in - - let u = get_univ univ in - let entryl = List.map (gram_define_entry u) astl in - { gc_univ = univ; - gc_entries = List.map (gram_entry u) entryl } - - -(* Converting and checking pretty-printing command *) - -type precedence = int * int * int -type parenRelation = L | E | Any | Prec of precedence - -let compare_prec (a1,b1,c1) (a2,b2,c2) = - match (a1=a2),(b1=b2),(c1=c2) with - | true,true,true -> 0 - | true,true,false -> c1-c2 - | true,false,_ -> b1-b2 - | false,_,_ -> a1-a2 - -let tolerable_prec oparent_prec_reln (_,child_prec) = - match oparent_prec_reln with - | Some ((_,pprec), L) -> (compare_prec child_prec pprec) < 0 - | Some ((_,pprec), E) -> (compare_prec child_prec pprec) <= 0 - | Some (_, Prec level) -> (compare_prec child_prec level) <= 0 - | _ -> true - -type ppbox = - | PpHB of int - | PpHOVB of int - | PpHVB of int - | PpVB of int - | PpTB - -type tolerability = (string * precedence) * parenRelation - -type unparsing_hunk = - | PH of Ast.pat * string option * parenRelation - | RO of string - | UNP_BOX of ppbox * unparsing_hunk list - | UNP_BRK of int * int - | UNP_TBRK of int * int - | UNP_TAB - | UNP_FNL - -let ppcmd_of_box = function - | PpHB n -> h n - | PpHOVB n -> hov n - | PpHVB n -> hv n - | PpVB n -> v n - | PpTB -> t - -(* Parsing the unparsing specifications *) - -let box_of_ast = function - | Node (_, "PpHB", [Num (_, n)]) -> (PpHB n) - | Node (_, "PpHOVB", [Num (_, n)]) -> (PpHOVB n) - | Node (_, "PpHVB", [Num (_, n)]) -> (PpHVB n) - | Node (_, "PpVB", [Num (_, n)]) -> (PpVB n) - | Node (_, "PpTB", []) -> PpTB - | p -> invalid_arg_loc (Ast.loc p,"Syntaxext.box_of_ast") - -let prec_of_ast = function - | Node(_,"PREC",[Num(_,a1); Num(_,a2); Num(_,a3)]) -> (a1,a2,a3) - | ast -> invalid_arg_loc (Ast.loc ast,"Syntaxext.prec_of_ast") - -let extern_of_ast loc = function - | [Str(_,ppextern)] -> (ppextern, Any) - | [Str(_,ppextern);p] -> - (ppextern, Prec (prec_of_ast p)) - | _ -> invalid_arg_loc (loc,"Syntaxext.extern_of_ast") - -let rec unparsing_hunk_of_ast vars = function - | Node(_, "PH", [e; Node (loc,"EXTERN", ext_args)]) -> - let (ppex, rel) = extern_of_ast loc ext_args in - PH (Ast.val_of_ast vars e, Some ppex, rel) - | Node(loc, "PH", [e; Node(_,pr, [])]) -> - let reln = - (match pr with - | "L" -> L - | "E" -> E - | "Any" -> Any - | _ -> invalid_arg_loc (loc,"Syntaxext.paren_reln_of_ast")) in - PH (Ast.val_of_ast vars e, None, reln) - | Node (_, "RO", [Str(_,s)]) -> RO s - | Node (_, "UNP_FNL", []) -> UNP_FNL - | Node (_, "UNP_TAB", []) -> UNP_TAB - | Node (_, "UNP_BRK", [Num(_, n1); Num(_, n2)]) -> UNP_BRK(n1,n2) - | Node (_, "UNP_TBRK", [Num(_, n1); Num(_, n2)]) -> UNP_TBRK(n1,n2) - | Node (_, "UNP_BOX", (box::sub)) -> - UNP_BOX(box_of_ast box, - List.map (unparsing_hunk_of_ast vars) sub) - | h -> invalid_arg_loc (Ast.loc h,"Syntaxext.unparsing_hunk_of_ast") - -let unparsing_of_ast vars = function - | Node(_,"UNPARSING",ll) -> - List.map (unparsing_hunk_of_ast vars) ll - | u -> invalid_arg_loc (Ast.loc u,"Syntaxext.unp_of_ast") - -type syntax_entry = { - syn_id : string; - syn_prec: precedence; - syn_astpat : Ast.pat; - syn_hunks : unparsing_hunk list } - -type syntax_command = { - sc_univ : string; - sc_entries : syntax_entry list } - -let rule_of_ast whatfor prec = function - | Node(_,"SYNTAXRULE",[Id(_,s); spat; unp]) -> - let (astpat,meta_env) = Ast.to_pat [] spat in - let hunks = unparsing_of_ast meta_env unp in - { syn_id = s; - syn_prec = prec; - syn_astpat = astpat; - syn_hunks = hunks } - | ast -> invalid_arg_loc (Ast.loc ast,"Metasyntax.rule_of_ast") - -let level_of_ast whatfor = function - | Node(_,"SYNTAXENTRY",(pr::rl)) -> - let prec = prec_of_ast pr in - List.map (rule_of_ast whatfor prec) rl - | ast -> invalid_arg_loc (Ast.loc ast,"Metasyntax.level_of_ast") - -let interp_syntax_entry univ sel = - { sc_univ = univ; - sc_entries = List.flatten (List.map (level_of_ast univ) sel)} - - diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 34afd2200d..f15ac3d78f 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -19,7 +19,7 @@ open Unix (* 1. Core objects *) let ocamlobjs = ["unix.cma"] let dynobjs = ["dynlink.cma"] -let camlp4objs = ["gramlib.cma"] +let camlp4objs = [(*"odyl.cma"; "camlp4.cma";*) "gramlib.cma"] let configobjs = ["coq_config.cmo"] let libobjs = ocamlobjs @ camlp4objs @ configobjs @@ -34,6 +34,7 @@ let parsing = split_cmo Tolink.parsing let proofs = split_cmo Tolink.proofs let tactics = split_cmo Tolink.tactics let toplevel = split_cmo Tolink.toplevel +let highparsing = split_cmo Tolink.highparsing let core_objs = libobjs @ lib @ kernel @ library @ pretyping @ parsing @ @@ -44,8 +45,7 @@ let coqsearch = ["version_searchisos.cmo"; "cmd_searchisos_line.cmo"] (* 4. Toplevel objects *) let camlp4objs = - ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"; - "q_coqast.cmo" ] + ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"; "q_util.cmo"; "q_coqast.cmo" ] let topobjs = camlp4objs let gramobjs = [] @@ -92,8 +92,8 @@ let files_to_link userfiles = let command_objs = if !searchisos then coqsearch else [] in let toplevel_objs = if !top then topobjs else if !opt then notopobjs else [] in - let objs = core_objs @ dyn_objs @ toplevel @ command_objs @ hightactics @ - toplevel_objs in + let objs = core_objs @ dyn_objs @ toplevel @ highparsing @ + command_objs @ hightactics @ toplevel_objs in let tolink = if !opt then (List.map native_suffix objs) @ userfiles diff --git a/states/MakeInitial.v b/states/MakeInitial.v index 3997ae3212..02235e1b8a 100644 --- a/states/MakeInitial.v +++ b/states/MakeInitial.v @@ -8,11 +8,3 @@ Require Export Prelude. Require Export Logic_Type. Require Export Logic_TypeSyntax. -Require Export Equality. -Require Export Tauto. -Require Export Inv. -Require Export EAuto. -Require Export AutoRewrite. -Require Export Refine. -Require Export EqDecide. -Require Export Extraction. diff --git a/syntax/MakeBare.v b/syntax/MakeBare.v index 17a5e04a64..0ab1ac6bb6 100644 --- a/syntax/MakeBare.v +++ b/syntax/MakeBare.v @@ -7,4 +7,3 @@ (***********************************************************************) Load PPConstr. Load PPCases. -Load PPTactic. diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml deleted file mode 100644 index 4675f9c8a3..0000000000 --- a/tactics/tacentries.ml +++ /dev/null @@ -1,58 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* tactic -val v_contradiction : tactic_arg list -> tactic -val v_reflexivity : tactic_arg list -> tactic -val v_symmetry : tactic_arg list -> tactic -val v_transitivity : tactic_arg list -> tactic -val v_intro : tactic_arg list -> tactic -val v_introsUntil : tactic_arg list -> tactic -(*i val v_tclIDTAC : tactic_arg list -> tactic i*) -val v_assumption : tactic_arg list -> tactic -val v_exact : tactic_arg list -> tactic -val v_reduce : tactic_arg list -> tactic -val v_constructor : tactic_arg list -> tactic -val v_left : tactic_arg list -> tactic -val v_right : tactic_arg list -> tactic -val v_split : tactic_arg list -> tactic -val v_clear : tactic_arg list -> tactic -val v_clear_body : tactic_arg list -> tactic -val v_move : tactic_arg list -> tactic -val v_move_dep : tactic_arg list -> tactic -val v_apply : tactic_arg list -> tactic -val v_cutAndResolve : tactic_arg list -> tactic -val v_cut : tactic_arg list -> tactic -val v_truecut : tactic_arg list -> tactic -val v_lettac : tactic_arg list -> tactic -val v_generalize : tactic_arg list -> tactic -val v_generalize_dep : tactic_arg list -> tactic -val v_specialize : tactic_arg list -> tactic -val v_elim : tactic_arg list -> tactic -val v_elimType : tactic_arg list -> tactic -val v_induction : tactic_arg list -> tactic -(*i val v_new_induction : tactic_arg list -> tactic i*) -val v_case : tactic_arg list -> tactic -val v_caseType : tactic_arg list -> tactic -val v_destruct : tactic_arg list -> tactic -(*i val v_new_destruct : tactic_arg list -> tactic i*) -val v_fix : tactic_arg list -> tactic -val v_cofix : tactic_arg list -> tactic -val vernac_instantiate : tactic_arg list -> tactic diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 99342140e4..042a18738a 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -128,8 +128,8 @@ let standard sds = let implicit () = let ml_rules () = print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; and v_rule () = print ".v.vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; print ".v.vi:\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; @@ -182,6 +182,10 @@ let variables l = print "CAMLOPTLINK=ocamlopt\n"; print "COQDEP=$(COQBIN)coqdep -c\n"; print "COQVO2XML=coq_vo2xml\n"; + print "GRAMMARS=grammar.cma g_constr.cmo g_tactic.cmo g_ltac.cmo \\ + g_basevernac.cmo tacextend.cmo vernacextend.cmo\n"; + print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n"; + print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; var_aux l; print "\n" -- cgit v1.2.3