diff options
| -rw-r--r-- | .depend | 708 | ||||
| -rw-r--r-- | Makefile | 16 | ||||
| -rw-r--r-- | contrib/correctness/pmlize.ml | 1 | ||||
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 4 | ||||
| -rw-r--r-- | contrib/correctness/putil.ml | 1 | ||||
| -rw-r--r-- | contrib/field/field.ml4 | 55 | ||||
| -rwxr-xr-x | contrib/interface/blast.ml | 5 | ||||
| -rw-r--r-- | contrib/interface/centaur.ml4 | 6 | ||||
| -rw-r--r-- | contrib/interface/dad.ml | 1 | ||||
| -rw-r--r-- | contrib/interface/debug_tac.ml4 | 40 | ||||
| -rw-r--r-- | contrib/interface/debug_tac.mli | 6 | ||||
| -rw-r--r-- | contrib/interface/pbp.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 4 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 1 | ||||
| -rw-r--r-- | contrib/xml/xmlentries.ml4 | 84 | ||||
| -rw-r--r-- | pretyping/matching.ml | 250 | ||||
| -rw-r--r-- | pretyping/matching.mli | 53 |
17 files changed, 749 insertions, 488 deletions
@@ -122,8 +122,8 @@ parsing/ppconstr.cmi: parsing/coqast.cmi kernel/environ.cmi \ lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi \ interp/topconstr.cmi lib/util.cmi parsing/pptactic.cmi: parsing/egrammar.cmi interp/genarg.cmi lib/pp.cmi \ - pretyping/pretyping.cmi proofs/proof_type.cmi proofs/tacexpr.cmo \ - kernel/term.cmi interp/topconstr.cmi + pretyping/pretyping.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ + proofs/tacexpr.cmo kernel/term.cmi interp/topconstr.cmi lib/util.cmi parsing/prettyp.cmi: pretyping/classops.cmi kernel/environ.cmi \ library/impargs.cmi library/lib.cmi library/libnames.cmi kernel/names.cmi \ library/nametab.cmi lib/pp.cmi pretyping/reductionops.cmi \ @@ -168,9 +168,11 @@ pretyping/inductiveops.cmi: kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi pretyping/instantiate.cmi: kernel/environ.cmi pretyping/evd.cmi \ kernel/names.cmi kernel/sign.cmi kernel/term.cmi -pretyping/pattern.cmi: kernel/environ.cmi pretyping/evd.cmi \ - library/libnames.cmi kernel/names.cmi library/nametab.cmi \ - pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi +pretyping/matching.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ + pretyping/pattern.cmi kernel/term.cmi +pretyping/pattern.cmi: kernel/environ.cmi library/libnames.cmi \ + kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \ + kernel/sign.cmi kernel/term.cmi pretyping/pretype_errors.cmi: kernel/environ.cmi pretyping/evd.cmi \ pretyping/inductiveops.cmi kernel/names.cmi lib/pp.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi @@ -211,8 +213,9 @@ 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/environ.cmi pretyping/evd.cmi interp/genarg.cmi \ - library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \ - proofs/tacexpr.cmo kernel/term.cmi lib/util.cmi + library/libnames.cmi kernel/names.cmi library/nametab.cmi \ + pretyping/pattern.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 proofs/tacexpr.cmo kernel/term.cmi proofs/tacmach.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ @@ -264,8 +267,8 @@ tactics/refine.cmi: pretyping/pretyping.cmi proofs/tacmach.cmi \ tactics/setoid_replace.cmi: kernel/names.cmi proofs/proof_type.cmi \ kernel/term.cmi interp/topconstr.cmi tactics/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \ - pretyping/evd.cmi interp/genarg.cmi kernel/names.cmi lib/pp.cmi \ - proofs/proof_type.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ + pretyping/evd.cmi interp/genarg.cmi kernel/names.cmi library/nametab.cmi \ + lib/pp.cmi proofs/proof_type.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ pretyping/tacred.cmi proofs/tactic_debug.cmi kernel/term.cmi \ interp/topconstr.cmi lib/util.cmi tactics/tacticals.cmi: proofs/clenv.cmi kernel/names.cmi \ @@ -315,9 +318,10 @@ toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: proofs/tacexpr.cmo translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \ - parsing/extend.cmi library/libnames.cmi kernel/names.cmi parsing/pcoq.cmi \ - lib/pp.cmi interp/ppextend.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \ - kernel/term.cmi interp/topconstr.cmi lib/util.cmi + parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \ + kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi interp/ppextend.cmi \ + pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi \ + interp/topconstr.cmi lib/util.cmi translate/pptacticnew.cmi: kernel/environ.cmi interp/genarg.cmi lib/pp.cmi \ proofs/proof_type.cmi proofs/tacexpr.cmo interp/topconstr.cmi translate/ppvernacnew.cmi: parsing/ast.cmi parsing/coqast.cmi \ @@ -441,18 +445,18 @@ 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/closure.cmi kernel/environ.cmi pretyping/evd.cmi \ - library/libnames.cmi library/libobject.cmi library/nameops.cmi \ - kernel/names.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 \ + kernel/closure.cmi interp/constrextern.cmi kernel/environ.cmi \ + pretyping/evd.cmi library/libnames.cmi library/libobject.cmi \ + library/nameops.cmi kernel/names.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 \ pretyping/termops.cmi kernel/univ.cmi dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \ - kernel/closure.cmx kernel/environ.cmx pretyping/evd.cmx \ - library/libnames.cmx library/libobject.cmx library/nameops.cmx \ - kernel/names.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 \ + kernel/closure.cmx interp/constrextern.cmx kernel/environ.cmx \ + pretyping/evd.cmx library/libnames.cmx library/libobject.cmx \ + library/nameops.cmx kernel/names.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 \ pretyping/termops.cmx kernel/univ.cmx doc/parse.cmo: parsing/ast.cmi doc/parse.cmx: parsing/ast.cmx @@ -926,18 +930,22 @@ parsing/g_constrnew.cmx: lib/bignat.cmx parsing/lexer.cmx \ library/libnames.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \ lib/pp.cmx pretyping/rawterm.cmx kernel/term.cmx interp/topconstr.cmx \ lib/util.cmx -parsing/g_ltac.cmo: parsing/ast.cmi library/libnames.cmi kernel/names.cmi \ - parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \ - interp/topconstr.cmi lib/util.cmi toplevel/vernacexpr.cmo -parsing/g_ltac.cmx: parsing/ast.cmx library/libnames.cmx kernel/names.cmx \ - parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \ - interp/topconstr.cmx lib/util.cmx toplevel/vernacexpr.cmx -parsing/g_ltacnew.cmo: parsing/ast.cmi kernel/names.cmi parsing/pcoq.cmi \ - lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo interp/topconstr.cmi \ - lib/util.cmi toplevel/vernacexpr.cmo -parsing/g_ltacnew.cmx: parsing/ast.cmx kernel/names.cmx parsing/pcoq.cmx \ - lib/pp.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx interp/topconstr.cmx \ - lib/util.cmx toplevel/vernacexpr.cmx +parsing/g_ltac.cmo: parsing/ast.cmi interp/genarg.cmi library/libnames.cmi \ + kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \ + proofs/tacexpr.cmo interp/topconstr.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo +parsing/g_ltac.cmx: parsing/ast.cmx interp/genarg.cmx library/libnames.cmx \ + kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx \ + proofs/tacexpr.cmx interp/topconstr.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx +parsing/g_ltacnew.cmo: parsing/ast.cmi interp/genarg.cmi library/libnames.cmi \ + kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \ + proofs/tacexpr.cmo interp/topconstr.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo +parsing/g_ltacnew.cmx: parsing/ast.cmx interp/genarg.cmx library/libnames.cmx \ + kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx \ + proofs/tacexpr.cmx interp/topconstr.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 @@ -1080,26 +1088,26 @@ parsing/pcoq.cmx: parsing/ast.cmx parsing/coqast.cmx library/decl_kinds.cmx \ library/libnames.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ interp/ppextend.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \ interp/topconstr.cmx lib/util.cmx parsing/pcoq.cmi -parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi parsing/coqast.cmi \ - interp/genarg.cmi library/libnames.cmi library/nameops.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi interp/ppextend.cmi \ - pretyping/rawterm.cmi interp/symbols.cmi kernel/term.cmi \ - interp/topconstr.cmi lib/util.cmi parsing/ppconstr.cmi -parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \ - interp/genarg.cmx library/libnames.cmx library/nameops.cmx \ - kernel/names.cmx library/nametab.cmx lib/pp.cmx interp/ppextend.cmx \ - pretyping/rawterm.cmx interp/symbols.cmx kernel/term.cmx \ - interp/topconstr.cmx lib/util.cmx parsing/ppconstr.cmi +parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi interp/constrextern.cmi \ + parsing/coqast.cmi interp/genarg.cmi library/libnames.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + interp/ppextend.cmi pretyping/rawterm.cmi interp/symbols.cmi \ + kernel/term.cmi interp/topconstr.cmi lib/util.cmi parsing/ppconstr.cmi +parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx interp/constrextern.cmx \ + parsing/coqast.cmx interp/genarg.cmx library/libnames.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + interp/ppextend.cmx pretyping/rawterm.cmx interp/symbols.cmx \ + kernel/term.cmx interp/topconstr.cmx lib/util.cmx parsing/ppconstr.cmi parsing/pptactic.cmo: kernel/closure.cmi lib/dyn.cmi parsing/egrammar.cmi \ parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \ - library/nameops.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ - parsing/ppconstr.cmi parsing/printer.cmi pretyping/rawterm.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + lib/pp.cmi parsing/ppconstr.cmi parsing/printer.cmi pretyping/rawterm.cmi \ proofs/tacexpr.cmo kernel/term.cmi interp/topconstr.cmi lib/util.cmi \ parsing/pptactic.cmi parsing/pptactic.cmx: kernel/closure.cmx lib/dyn.cmx parsing/egrammar.cmx \ parsing/extend.cmx interp/genarg.cmx library/libnames.cmx \ - library/nameops.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ - parsing/ppconstr.cmx parsing/printer.cmx pretyping/rawterm.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + lib/pp.cmx parsing/ppconstr.cmx parsing/printer.cmx pretyping/rawterm.cmx \ proofs/tacexpr.cmx kernel/term.cmx interp/topconstr.cmx lib/util.cmx \ parsing/pptactic.cmi parsing/prettyp.cmo: pretyping/classops.cmi interp/constrextern.cmi \ @@ -1154,48 +1162,50 @@ parsing/search.cmo: parsing/coqast.cmi interp/coqlib.cmi \ kernel/declarations.cmi library/declare.cmi library/declaremods.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ library/libnames.cmi library/libobject.cmi library/library.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi \ - pretyping/pattern.cmi lib/pp.cmi pretyping/pretyping.cmi \ - parsing/printer.cmi pretyping/rawterm.cmi pretyping/retyping.cmi \ - kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ - parsing/search.cmi + pretyping/matching.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \ + pretyping/pretyping.cmi parsing/printer.cmi pretyping/rawterm.cmi \ + pretyping/retyping.cmi kernel/term.cmi pretyping/termops.cmi \ + pretyping/typing.cmi lib/util.cmi parsing/search.cmi parsing/search.cmx: parsing/coqast.cmx interp/coqlib.cmx \ kernel/declarations.cmx library/declare.cmx library/declaremods.cmx \ kernel/environ.cmx pretyping/evd.cmx library/global.cmx \ library/libnames.cmx library/libobject.cmx library/library.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx \ - pretyping/pattern.cmx lib/pp.cmx pretyping/pretyping.cmx \ - parsing/printer.cmx pretyping/rawterm.cmx pretyping/retyping.cmx \ - kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ - parsing/search.cmi -parsing/tacextend.cmo: interp/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: interp/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/matching.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \ + pretyping/pretyping.cmx parsing/printer.cmx pretyping/rawterm.cmx \ + pretyping/retyping.cmx kernel/term.cmx pretyping/termops.cmx \ + pretyping/typing.cmx lib/util.cmx parsing/search.cmi +parsing/tacextend.cmo: parsing/argextend.cmo interp/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/argextend.cmx interp/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 \ - library/libnames.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \ + interp/constrextern.cmi parsing/coqast.cmi library/declare.cmi \ + pretyping/detyping.cmi kernel/environ.cmi library/impargs.cmi \ + kernel/inductive.cmi library/libnames.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \ pretyping/rawterm.cmi pretyping/reductionops.cmi kernel/sign.cmi \ kernel/term.cmi pretyping/termops.cmi kernel/univ.cmi lib/util.cmi \ parsing/termast.cmi parsing/termast.cmx: parsing/ast.cmx pretyping/classops.cmx \ - parsing/coqast.cmx library/declare.cmx pretyping/detyping.cmx \ - kernel/environ.cmx library/impargs.cmx kernel/inductive.cmx \ - library/libnames.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \ + interp/constrextern.cmx parsing/coqast.cmx library/declare.cmx \ + pretyping/detyping.cmx kernel/environ.cmx library/impargs.cmx \ + kernel/inductive.cmx library/libnames.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.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 interp/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 interp/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/vernacextend.cmo: parsing/argextend.cmo parsing/ast.cmi \ + interp/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/argextend.cmx parsing/ast.cmx \ + interp/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 \ @@ -1316,14 +1326,22 @@ pretyping/instantiate.cmo: kernel/declarations.cmi kernel/environ.cmi \ pretyping/instantiate.cmx: kernel/declarations.cmx kernel/environ.cmx \ pretyping/evd.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \ kernel/term.cmx lib/util.cmx pretyping/instantiate.cmi -pretyping/pattern.cmo: kernel/environ.cmi library/libnames.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi \ +pretyping/matching.cmo: kernel/environ.cmi library/libnames.cmi \ + library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi \ pretyping/rawterm.cmi pretyping/reductionops.cmi kernel/term.cmi \ - pretyping/termops.cmi lib/util.cmi pretyping/pattern.cmi -pretyping/pattern.cmx: kernel/environ.cmx library/libnames.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx \ + pretyping/termops.cmi lib/util.cmi pretyping/matching.cmi +pretyping/matching.cmx: kernel/environ.cmx library/libnames.cmx \ + library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx \ pretyping/rawterm.cmx pretyping/reductionops.cmx kernel/term.cmx \ - pretyping/termops.cmx lib/util.cmx pretyping/pattern.cmi + pretyping/termops.cmx lib/util.cmx pretyping/matching.cmi +pretyping/pattern.cmo: kernel/environ.cmi library/libnames.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + lib/pp.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \ + pretyping/pattern.cmi +pretyping/pattern.cmx: kernel/environ.cmx library/libnames.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + lib/pp.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \ + pretyping/pattern.cmi pretyping/pretype_errors.cmo: kernel/environ.cmi pretyping/evd.cmi \ pretyping/inductiveops.cmi kernel/names.cmi pretyping/rawterm.cmi \ kernel/reduction.cmi pretyping/reductionops.cmi kernel/sign.cmi \ @@ -1454,20 +1472,20 @@ proofs/logic.cmo: interp/constrextern.cmi 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 kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ - kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \ - kernel/type_errors.cmi kernel/typeops.cmi pretyping/typing.cmi \ - lib/util.cmi proofs/logic.cmi + library/nametab.cmi lib/pp.cmi pretyping/pretype_errors.cmi \ + parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + pretyping/reductionops.cmi pretyping/retyping.cmi kernel/sign.cmi \ + kernel/term.cmi pretyping/termops.cmi kernel/type_errors.cmi \ + kernel/typeops.cmi pretyping/typing.cmi lib/util.cmi proofs/logic.cmi proofs/logic.cmx: interp/constrextern.cmx parsing/coqast.cmx \ library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \ pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \ pretyping/inductiveops.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ - kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ - kernel/type_errors.cmx kernel/typeops.cmx pretyping/typing.cmx \ - lib/util.cmx proofs/logic.cmi + library/nametab.cmx lib/pp.cmx pretyping/pretype_errors.cmx \ + parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + pretyping/reductionops.cmx pretyping/retyping.cmx kernel/sign.cmx \ + kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx \ + kernel/typeops.cmx pretyping/typing.cmx lib/util.cmx proofs/logic.cmi proofs/pfedit.cmo: library/decl_kinds.cmo kernel/declarations.cmi \ library/declare.cmi lib/edit.cmi kernel/entries.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi library/lib.cmi \ @@ -1497,11 +1515,13 @@ proofs/proof_trees.cmx: kernel/closure.cmx pretyping/detyping.cmx \ kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ proofs/proof_trees.cmi proofs/proof_type.cmo: kernel/environ.cmi pretyping/evd.cmi interp/genarg.cmi \ - library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \ - proofs/tacexpr.cmo kernel/term.cmi lib/util.cmi proofs/proof_type.cmi + library/libnames.cmi kernel/names.cmi library/nametab.cmi \ + pretyping/pattern.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \ + kernel/term.cmi lib/util.cmi proofs/proof_type.cmi proofs/proof_type.cmx: kernel/environ.cmx pretyping/evd.cmx interp/genarg.cmx \ - library/libnames.cmx kernel/names.cmx pretyping/rawterm.cmx \ - proofs/tacexpr.cmx kernel/term.cmx lib/util.cmx proofs/proof_type.cmi + library/libnames.cmx kernel/names.cmx library/nametab.cmx \ + pretyping/pattern.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \ + kernel/term.cmx lib/util.cmx proofs/proof_type.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/pptactic.cmi parsing/printer.cmi \ @@ -1516,10 +1536,18 @@ proofs/refiner.cmx: kernel/environ.cmx pretyping/evarutil.cmx \ kernel/type_errors.cmx lib/util.cmx proofs/refiner.cmi proofs/tacexpr.cmo: library/decl_kinds.cmo lib/dyn.cmi interp/genarg.cmi \ library/libnames.cmi kernel/names.cmi library/nametab.cmi \ - pretyping/rawterm.cmi interp/topconstr.cmi lib/util.cmi + pretyping/pattern.cmi pretyping/rawterm.cmi kernel/term.cmi \ + interp/topconstr.cmi lib/util.cmi proofs/tacexpr.cmx: library/decl_kinds.cmx lib/dyn.cmx interp/genarg.cmx \ library/libnames.cmx kernel/names.cmx library/nametab.cmx \ - pretyping/rawterm.cmx interp/topconstr.cmx lib/util.cmx + pretyping/pattern.cmx pretyping/rawterm.cmx kernel/term.cmx \ + interp/topconstr.cmx lib/util.cmx +proofs/tacintern.cmo: interp/constrintern.cmi kernel/environ.cmi \ + pretyping/evd.cmi library/global.cmi proofs/logic.cmi library/nametab.cmi \ + proofs/pfedit.cmi pretyping/pretype_errors.cmi +proofs/tacintern.cmx: interp/constrintern.cmx kernel/environ.cmx \ + pretyping/evd.cmx library/global.cmx proofs/logic.cmx library/nametab.cmx \ + proofs/pfedit.cmx pretyping/pretype_errors.cmx proofs/tacmach.cmo: interp/constrintern.cmi library/declare.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ pretyping/instantiate.cmi proofs/logic.cmi library/nameops.cmi \ @@ -1553,29 +1581,29 @@ tactics/auto.cmo: tactics/btermdn.cmi proofs/clenv.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \ tactics/hiddentac.cmi tactics/hipattern.cmi kernel/inductive.cmi \ library/lib.cmi library/libnames.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 + library/library.cmi proofs/logic.cmi pretyping/matching.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: tactics/btermdn.cmx proofs/clenv.cmx \ interp/constrintern.cmx kernel/declarations.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/libnames.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 + library/library.cmx proofs/logic.cmx pretyping/matching.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 \ @@ -1603,73 +1631,79 @@ tactics/contradiction.cmx: interp/coqlib.cmx tactics/hipattern.cmx \ tactics/dhyp.cmo: parsing/ast.cmi proofs/clenv.cmi interp/constrintern.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi library/lib.cmi \ library/libnames.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 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 + pretyping/matching.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 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 proofs/clenv.cmx interp/constrintern.cmx \ kernel/environ.cmx pretyping/evd.cmx library/global.cmx library/lib.cmx \ library/libnames.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 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 + pretyping/matching.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 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 toplevel/cerrors.cmi proofs/clenv.cmi \ parsing/egrammar.cmi proofs/evar_refiner.cmi lib/explore.cmi \ - interp/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 + parsing/extend.cmi interp/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 \ - interp/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 library/libnames.cmi \ - kernel/names.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \ - pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \ + parsing/extend.cmx interp/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 interp/genarg.cmi \ + tactics/hiddentac.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \ + library/libnames.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_type.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 kernel/environ.cmx tactics/hiddentac.cmx \ - tactics/hipattern.cmx pretyping/inductiveops.cmx library/libnames.cmx \ - kernel/names.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \ - pretyping/rawterm.cmx kernel/reduction.cmx proofs/refiner.cmx \ +tactics/elim.cmx: proofs/clenv.cmx kernel/environ.cmx interp/genarg.cmx \ + tactics/hiddentac.cmx tactics/hipattern.cmx pretyping/inductiveops.cmx \ + library/libnames.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_type.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 toplevel/cerrors.cmi interp/coqlib.cmi \ kernel/declarations.cmi parsing/egrammar.cmi tactics/equality.cmi \ tactics/extratactics.cmi interp/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 \ - pretyping/rawterm.cmi proofs/refiner.cmi proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi + tactics/hiddentac.cmi tactics/hipattern.cmi pretyping/matching.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 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 interp/coqlib.cmx \ kernel/declarations.cmx parsing/egrammar.cmx tactics/equality.cmx \ tactics/extratactics.cmx interp/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 \ - pretyping/rawterm.cmx proofs/refiner.cmx proofs/tacmach.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx + tactics/hiddentac.cmx tactics/hipattern.cmx pretyping/matching.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 proofs/refiner.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx lib/util.cmx tactics/equality.cmo: proofs/clenv.cmi interp/coqlib.cmi \ kernel/declarations.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ pretyping/evarutil.cmi tactics/hipattern.cmi pretyping/indrec.cmi \ kernel/inductive.cmi pretyping/inductiveops.cmi pretyping/instantiate.cmi \ - proofs/logic.cmi library/nameops.cmi kernel/names.cmi \ - pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ + proofs/logic.cmi pretyping/matching.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 kernel/sign.cmi proofs/tacexpr.cmo \ tactics/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ @@ -1681,8 +1715,8 @@ tactics/equality.cmx: proofs/clenv.cmx interp/coqlib.cmx \ kernel/declarations.cmx kernel/environ.cmx proofs/evar_refiner.cmx \ pretyping/evarutil.cmx tactics/hipattern.cmx pretyping/indrec.cmx \ kernel/inductive.cmx pretyping/inductiveops.cmx pretyping/instantiate.cmx \ - proofs/logic.cmx library/nameops.cmx kernel/names.cmx \ - pretyping/pattern.cmx lib/pp.cmx proofs/proof_type.cmx \ + proofs/logic.cmx pretyping/matching.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 kernel/sign.cmx proofs/tacexpr.cmx \ tactics/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ @@ -1691,13 +1725,11 @@ tactics/equality.cmx: proofs/clenv.cmx interp/coqlib.cmx \ kernel/univ.cmx lib/util.cmx toplevel/vernacexpr.cmx \ toplevel/vernacinterp.cmx tactics/wcclausenv.cmx tactics/equality.cmi tactics/extraargs.cmo: parsing/extend.cmi interp/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 + toplevel/metasyntax.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \ + tactics/tacinterp.cmi tactics/extraargs.cmi tactics/extraargs.cmx: parsing/extend.cmx interp/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 + toplevel/metasyntax.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \ + tactics/tacinterp.cmx tactics/extraargs.cmi tactics/extratactics.cmo: tactics/autorewrite.cmi toplevel/cerrors.cmi \ interp/constrintern.cmi tactics/contradiction.cmi parsing/egrammar.cmi \ tactics/equality.cmi pretyping/evd.cmi tactics/extraargs.cmi \ @@ -1714,44 +1746,46 @@ tactics/extratactics.cmx: tactics/autorewrite.cmx toplevel/cerrors.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/hiddentac.cmo: proofs/evar_refiner.cmi interp/genarg.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 interp/genarg.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 interp/coqlib.cmi \ kernel/declarations.cmi kernel/environ.cmi pretyping/evd.cmi \ - library/global.cmi pretyping/inductiveops.cmi library/nameops.cmi \ - kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ - pretyping/reductionops.cmi kernel/term.cmi pretyping/termops.cmi \ - lib/util.cmi tactics/hipattern.cmi + library/global.cmi pretyping/inductiveops.cmi pretyping/matching.cmi \ + library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ + proofs/proof_trees.cmi pretyping/reductionops.cmi kernel/term.cmi \ + pretyping/termops.cmi lib/util.cmi tactics/hipattern.cmi tactics/hipattern.cmx: proofs/clenv.cmx interp/coqlib.cmx \ kernel/declarations.cmx kernel/environ.cmx pretyping/evd.cmx \ - library/global.cmx pretyping/inductiveops.cmx library/nameops.cmx \ - kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ - pretyping/reductionops.cmx kernel/term.cmx pretyping/termops.cmx \ - lib/util.cmx tactics/hipattern.cmi + library/global.cmx pretyping/inductiveops.cmx pretyping/matching.cmx \ + library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ + proofs/proof_trees.cmx pretyping/reductionops.cmx kernel/term.cmx \ + pretyping/termops.cmx lib/util.cmx tactics/hipattern.cmi tactics/inv.cmo: proofs/clenv.cmi interp/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 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 + library/global.cmi pretyping/inductiveops.cmi pretyping/matching.cmi \ + library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ + parsing/printer.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 interp/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 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 + library/global.cmx pretyping/inductiveops.cmx pretyping/matching.cmx \ + library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ + parsing/printer.cmx 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: proofs/clenv.cmi interp/constrintern.cmi \ library/decl_kinds.cmo kernel/declarations.cmi library/declare.cmi \ kernel/entries.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ @@ -1785,21 +1819,21 @@ tactics/newtauto.cmo: parsing/ast.cmi toplevel/cerrors.cmi parsing/coqast.cmi \ pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ tactics/hipattern.cmi pretyping/inductiveops.cmi library/libnames.cmi \ kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \ - parsing/printer.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ - pretyping/reductionops.cmi proofs/refiner.cmi kernel/sign.cmi \ - proofs/tacexpr.cmo tactics/tacinterp.cmi proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi tactics/tauto.cmo \ - kernel/term.cmi pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi + parsing/printer.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \ + proofs/refiner.cmi kernel/sign.cmi proofs/tacexpr.cmo \ + tactics/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi tactics/tauto.cmo kernel/term.cmi \ + pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi tactics/newtauto.cmx: parsing/ast.cmx toplevel/cerrors.cmx parsing/coqast.cmx \ kernel/declarations.cmx parsing/egrammar.cmx kernel/environ.cmx \ pretyping/evd.cmx interp/genarg.cmx library/global.cmx \ tactics/hipattern.cmx pretyping/inductiveops.cmx library/libnames.cmx \ kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \ - parsing/printer.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ - pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \ - proofs/tacexpr.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx tactics/tauto.cmx \ - kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx + parsing/printer.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \ + proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx \ + tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx tactics/tauto.cmx kernel/term.cmx \ + pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx 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 \ @@ -1842,44 +1876,46 @@ tactics/tacinterp.cmo: parsing/ast.cmi tactics/auto.cmi kernel/closure.cmi \ tactics/elim.cmi kernel/entries.cmi kernel/environ.cmi pretyping/evd.cmi \ interp/genarg.cmi library/global.cmi lib/gmap.cmi tactics/hiddentac.cmi \ library/lib.cmi library/libnames.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 \ + proofs/logic.cmi pretyping/matching.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 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 \ - pretyping/termops.cmi interp/topconstr.cmi pretyping/typing.cmi \ - lib/util.cmi tactics/tacinterp.cmi + pretyping/retyping.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 pretyping/termops.cmi interp/topconstr.cmi \ + pretyping/typing.cmi lib/util.cmi tactics/tacinterp.cmi tactics/tacinterp.cmx: parsing/ast.cmx tactics/auto.cmx kernel/closure.cmx \ interp/constrintern.cmx parsing/coqast.cmx library/decl_kinds.cmx \ kernel/declarations.cmx library/declare.cmx tactics/dhyp.cmx lib/dyn.cmx \ tactics/elim.cmx kernel/entries.cmx kernel/environ.cmx pretyping/evd.cmx \ interp/genarg.cmx library/global.cmx lib/gmap.cmx tactics/hiddentac.cmx \ library/lib.cmx library/libnames.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 \ + proofs/logic.cmx pretyping/matching.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 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 \ - pretyping/termops.cmx interp/topconstr.cmx pretyping/typing.cmx \ - lib/util.cmx tactics/tacinterp.cmi + pretyping/retyping.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 pretyping/termops.cmx interp/topconstr.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 \ - library/libnames.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 + library/libnames.cmi pretyping/matching.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 kernel/declarations.cmx \ library/declare.cmx kernel/environ.cmx proofs/evar_refiner.cmx \ library/global.cmx pretyping/indrec.cmx kernel/inductive.cmx \ - library/libnames.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 + library/libnames.cmx pretyping/matching.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: proofs/clenv.cmi interp/constrintern.cmi \ interp/coqlib.cmi library/decl_kinds.cmo kernel/declarations.cmi \ library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ @@ -2171,10 +2207,9 @@ toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \ kernel/safe_typing.cmi parsing/search.cmi library/states.cmi \ interp/symbols.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 \ - interp/topconstr.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \ - toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \ - toplevel/vernacentries.cmi + tactics/tactics.cmi kernel/term.cmi interp/topconstr.cmi \ + kernel/typeops.cmi kernel/univ.cmi lib/util.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacinterp.cmi toplevel/vernacentries.cmi toplevel/vernacentries.cmx: tactics/auto.cmx toplevel/class.cmx \ pretyping/classops.cmx toplevel/command.cmx interp/constrextern.cmx \ interp/constrintern.cmx library/decl_kinds.cmx library/declaremods.cmx \ @@ -2192,10 +2227,9 @@ toplevel/vernacentries.cmx: tactics/auto.cmx toplevel/class.cmx \ kernel/safe_typing.cmx parsing/search.cmx library/states.cmx \ interp/symbols.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 \ - interp/topconstr.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \ - toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx \ - toplevel/vernacentries.cmi + tactics/tactics.cmx kernel/term.cmx interp/topconstr.cmx \ + kernel/typeops.cmx kernel/univ.cmx lib/util.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacinterp.cmx toplevel/vernacentries.cmi toplevel/vernacexpr.cmo: library/decl_kinds.cmo parsing/extend.cmi \ interp/genarg.cmi library/goptions.cmi library/libnames.cmi \ kernel/names.cmi library/nametab.cmi interp/ppextend.cmi \ @@ -2232,38 +2266,42 @@ translate/ppconstrnew.cmx: parsing/ast.cmx lib/bignat.cmx \ pretyping/rawterm.cmx interp/reserve.cmx interp/symbols.cmx \ kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx \ translate/ppconstrnew.cmi -translate/pptacticnew.cmo: kernel/closure.cmi lib/dyn.cmi kernel/environ.cmi \ - parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \ - library/nameops.cmi kernel/names.cmi lib/pp.cmi translate/ppconstrnew.cmi \ - interp/ppextend.cmi parsing/pptactic.cmi pretyping/rawterm.cmi \ - proofs/tacexpr.cmo pretyping/termops.cmi interp/topconstr.cmi \ - lib/util.cmi translate/pptacticnew.cmi -translate/pptacticnew.cmx: kernel/closure.cmx lib/dyn.cmx kernel/environ.cmx \ - parsing/extend.cmx interp/genarg.cmx library/libnames.cmx \ - library/nameops.cmx kernel/names.cmx lib/pp.cmx translate/ppconstrnew.cmx \ - interp/ppextend.cmx parsing/pptactic.cmx pretyping/rawterm.cmx \ - proofs/tacexpr.cmx pretyping/termops.cmx interp/topconstr.cmx \ - lib/util.cmx translate/pptacticnew.cmi +translate/pptacticnew.cmo: kernel/closure.cmi lib/dyn.cmi \ + parsing/egrammar.cmi kernel/environ.cmi parsing/extend.cmi \ + interp/genarg.cmi library/libnames.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/pp.cmi translate/ppconstrnew.cmi \ + interp/ppextend.cmi parsing/pptactic.cmi parsing/printer.cmi \ + pretyping/rawterm.cmi proofs/tacexpr.cmo pretyping/termops.cmi \ + interp/topconstr.cmi lib/util.cmi translate/pptacticnew.cmi +translate/pptacticnew.cmx: kernel/closure.cmx lib/dyn.cmx \ + parsing/egrammar.cmx kernel/environ.cmx parsing/extend.cmx \ + interp/genarg.cmx library/libnames.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/pp.cmx translate/ppconstrnew.cmx \ + interp/ppextend.cmx parsing/pptactic.cmx parsing/printer.cmx \ + pretyping/rawterm.cmx proofs/tacexpr.cmx pretyping/termops.cmx \ + interp/topconstr.cmx lib/util.cmx translate/pptacticnew.cmi translate/ppvernacnew.cmo: parsing/ast.cmi interp/constrextern.cmi \ interp/constrintern.cmi parsing/coqast.cmi library/decl_kinds.cmo \ parsing/egrammar.cmi pretyping/evd.cmi parsing/extend.cmi \ - interp/genarg.cmi library/global.cmi library/goptions.cmi \ + interp/genarg.cmi library/global.cmi library/goptions.cmi library/lib.cmi \ library/libnames.cmi library/nameops.cmi kernel/names.cmi \ library/nametab.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ lib/pp.cmi translate/ppconstrnew.cmi interp/ppextend.cmi \ - translate/pptacticnew.cmi pretyping/rawterm.cmi interp/reserve.cmi \ - proofs/tacexpr.cmo pretyping/termops.cmi interp/topconstr.cmi \ - lib/util.cmi toplevel/vernacexpr.cmo translate/ppvernacnew.cmi + parsing/pptactic.cmi translate/pptacticnew.cmi pretyping/rawterm.cmi \ + interp/reserve.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \ + pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo translate/ppvernacnew.cmi translate/ppvernacnew.cmx: parsing/ast.cmx interp/constrextern.cmx \ interp/constrintern.cmx parsing/coqast.cmx library/decl_kinds.cmx \ parsing/egrammar.cmx pretyping/evd.cmx parsing/extend.cmx \ - interp/genarg.cmx library/global.cmx library/goptions.cmx \ + interp/genarg.cmx library/global.cmx library/goptions.cmx library/lib.cmx \ library/libnames.cmx library/nameops.cmx kernel/names.cmx \ library/nametab.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \ lib/pp.cmx translate/ppconstrnew.cmx interp/ppextend.cmx \ - translate/pptacticnew.cmx pretyping/rawterm.cmx interp/reserve.cmx \ - proofs/tacexpr.cmx pretyping/termops.cmx interp/topconstr.cmx \ - lib/util.cmx toplevel/vernacexpr.cmx translate/ppvernacnew.cmi + parsing/pptactic.cmx translate/pptacticnew.cmx pretyping/rawterm.cmx \ + interp/reserve.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \ + pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx translate/ppvernacnew.cmi contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi \ @@ -2381,23 +2419,25 @@ contrib/correctness/pmisc.cmx: library/declare.cmx pretyping/evarutil.cmx \ kernel/term.cmx interp/topconstr.cmx lib/util.cmx \ contrib/correctness/pmisc.cmi contrib/correctness/pmlize.cmo: interp/coqlib.cmi pretyping/evd.cmi \ - library/global.cmi kernel/names.cmi contrib/correctness/past.cmi \ - pretyping/pattern.cmi contrib/correctness/pcicenv.cmi \ - contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ - contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ - contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ - contrib/correctness/ptyping.cmi contrib/correctness/putil.cmi \ - pretyping/reductionops.cmi kernel/term.cmi parsing/termast.cmi \ - pretyping/typing.cmi lib/util.cmi contrib/correctness/pmlize.cmi + library/global.cmi pretyping/matching.cmi kernel/names.cmi \ + contrib/correctness/past.cmi pretyping/pattern.cmi \ + contrib/correctness/pcicenv.cmi contrib/correctness/peffect.cmi \ + contrib/correctness/penv.cmi contrib/correctness/pmisc.cmi \ + contrib/correctness/pmonad.cmi contrib/correctness/prename.cmi \ + contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmi \ + contrib/correctness/putil.cmi pretyping/reductionops.cmi kernel/term.cmi \ + parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \ + contrib/correctness/pmlize.cmi contrib/correctness/pmlize.cmx: interp/coqlib.cmx pretyping/evd.cmx \ - library/global.cmx kernel/names.cmx contrib/correctness/past.cmi \ - pretyping/pattern.cmx contrib/correctness/pcicenv.cmx \ - contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \ - contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ - contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ - contrib/correctness/ptyping.cmx contrib/correctness/putil.cmx \ - pretyping/reductionops.cmx kernel/term.cmx parsing/termast.cmx \ - pretyping/typing.cmx lib/util.cmx contrib/correctness/pmlize.cmi + library/global.cmx pretyping/matching.cmx kernel/names.cmx \ + contrib/correctness/past.cmi pretyping/pattern.cmx \ + contrib/correctness/pcicenv.cmx contrib/correctness/peffect.cmx \ + contrib/correctness/penv.cmx contrib/correctness/pmisc.cmx \ + contrib/correctness/pmonad.cmx contrib/correctness/prename.cmx \ + contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmx \ + contrib/correctness/putil.cmx pretyping/reductionops.cmx kernel/term.cmx \ + parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \ + contrib/correctness/pmlize.cmi contrib/correctness/pmonad.cmo: kernel/names.cmi contrib/correctness/past.cmi \ contrib/correctness/pcic.cmi contrib/correctness/peffect.cmi \ contrib/correctness/penv.cmi contrib/correctness/pmisc.cmi \ @@ -2507,15 +2547,15 @@ contrib/correctness/ptyping.cmx: interp/constrintern.cmx kernel/environ.cmx \ pretyping/termops.cmx interp/topconstr.cmx pretyping/typing.cmx \ lib/util.cmx contrib/correctness/ptyping.cmi contrib/correctness/putil.cmo: interp/coqlib.cmi kernel/environ.cmi \ - library/global.cmi library/nameops.cmi kernel/names.cmi \ - contrib/correctness/past.cmi pretyping/pattern.cmi \ + library/global.cmi pretyping/matching.cmi library/nameops.cmi \ + kernel/names.cmi contrib/correctness/past.cmi pretyping/pattern.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ contrib/correctness/pmisc.cmi lib/pp.cmi contrib/correctness/prename.cmi \ parsing/printer.cmi contrib/correctness/ptype.cmi kernel/term.cmi \ pretyping/termops.cmi lib/util.cmi contrib/correctness/putil.cmi contrib/correctness/putil.cmx: interp/coqlib.cmx kernel/environ.cmx \ - library/global.cmx library/nameops.cmx kernel/names.cmx \ - contrib/correctness/past.cmi pretyping/pattern.cmx \ + library/global.cmx pretyping/matching.cmx library/nameops.cmx \ + kernel/names.cmx contrib/correctness/past.cmi pretyping/pattern.cmx \ contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \ contrib/correctness/pmisc.cmx lib/pp.cmx contrib/correctness/prename.cmx \ parsing/printer.cmx contrib/correctness/ptype.cmi kernel/term.cmx \ @@ -2644,30 +2684,6 @@ contrib/extraction/table.cmx: kernel/declarations.cmx kernel/environ.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx library/summary.cmx \ kernel/term.cmx lib/util.cmx contrib/extraction/table.cmi -contrib/field/field.cmo: toplevel/cerrors.cmi interp/constrintern.cmi \ - interp/coqlib.cmi parsing/egrammar.cmi pretyping/evd.cmi \ - parsing/extend.cmi interp/genarg.cmi library/global.cmi lib/gmap.cmi \ - tactics/hipattern.cmi library/lib.cmi library/libnames.cmi \ - library/libobject.cmi library/library.cmi kernel/names.cmi \ - parsing/pcoq.cmi lib/pp.cmi translate/ppconstrnew.cmi \ - parsing/pptactic.cmi proofs/proof_type.cmi contrib/ring/quote.cmo \ - 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 \ - interp/topconstr.cmi pretyping/typing.cmi lib/util.cmi \ - toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi -contrib/field/field.cmx: toplevel/cerrors.cmx interp/constrintern.cmx \ - interp/coqlib.cmx parsing/egrammar.cmx pretyping/evd.cmx \ - parsing/extend.cmx interp/genarg.cmx library/global.cmx lib/gmap.cmx \ - tactics/hipattern.cmx library/lib.cmx library/libnames.cmx \ - library/libobject.cmx library/library.cmx kernel/names.cmx \ - parsing/pcoq.cmx lib/pp.cmx translate/ppconstrnew.cmx \ - parsing/pptactic.cmx proofs/proof_type.cmx contrib/ring/quote.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 \ - interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \ - toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx contrib/fourier/fourierR.cmo: proofs/clenv.cmi tactics/contradiction.cmi \ interp/coqlib.cmi tactics/equality.cmi contrib/fourier/fourier.cmo \ library/libnames.cmi library/library.cmi kernel/names.cmi \ @@ -2730,9 +2746,9 @@ contrib/interface/blast.cmo: tactics/auto.cmi proofs/clenv.cmi \ parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.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 \ + kernel/sign.cmi tactics/tacinterp.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: tactics/auto.cmx proofs/clenv.cmx \ @@ -2745,9 +2761,9 @@ contrib/interface/blast.cmx: tactics/auto.cmx proofs/clenv.cmx \ parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.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 \ + kernel/sign.cmx tactics/tacinterp.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 \ @@ -2798,22 +2814,22 @@ contrib/interface/ctast.cmx: parsing/coqast.cmx lib/dyn.cmx \ library/libnames.cmx kernel/names.cmx lib/util.cmx contrib/interface/dad.cmo: interp/constrextern.cmi interp/constrintern.cmi \ kernel/environ.cmi pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ - library/libnames.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/tacexpr.cmo proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - interp/topconstr.cmi pretyping/typing.cmi lib/util.cmi \ + library/libnames.cmi pretyping/matching.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/tacexpr.cmo \ + proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi interp/topconstr.cmi pretyping/typing.cmi lib/util.cmi \ toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \ contrib/interface/dad.cmi contrib/interface/dad.cmx: interp/constrextern.cmx interp/constrintern.cmx \ kernel/environ.cmx pretyping/evd.cmx interp/genarg.cmx library/global.cmx \ - library/libnames.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/tacexpr.cmx proofs/tacmach.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \ + library/libnames.cmx pretyping/matching.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/tacexpr.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx interp/topconstr.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 \ @@ -2869,23 +2885,25 @@ contrib/interface/parse.cmx: contrib/interface/ascent.cmi \ contrib/interface/paths.cmo: contrib/interface/paths.cmi contrib/interface/paths.cmx: contrib/interface/paths.cmi contrib/interface/pbp.cmo: interp/coqlib.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \ - library/libnames.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 interp/topconstr.cmi \ - pretyping/typing.cmi lib/util.cmi contrib/interface/pbp.cmi + pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ + tactics/hipattern.cmi library/libnames.cmi proofs/logic.cmi \ + pretyping/matching.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 interp/topconstr.cmi pretyping/typing.cmi lib/util.cmi \ + contrib/interface/pbp.cmi contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \ - pretyping/evd.cmx library/global.cmx tactics/hipattern.cmx \ - library/libnames.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 interp/topconstr.cmx \ - pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi + pretyping/evd.cmx interp/genarg.cmx library/global.cmx \ + tactics/hipattern.cmx library/libnames.cmx proofs/logic.cmx \ + pretyping/matching.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 interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \ + contrib/interface/pbp.cmi contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \ parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ @@ -3090,14 +3108,14 @@ contrib/ring/g_ring.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ toplevel/vernacinterp.cmx contrib/ring/quote.cmo: interp/coqlib.cmi kernel/environ.cmi \ library/global.cmi pretyping/instantiate.cmi library/library.cmi \ - kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ - proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/termops.cmi lib/util.cmi + pretyping/matching.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.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: interp/coqlib.cmx kernel/environ.cmx \ library/global.cmx pretyping/instantiate.cmx library/library.cmx \ - kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ - proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/termops.cmx lib/util.cmx + pretyping/matching.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.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: kernel/closure.cmi interp/constrintern.cmi \ interp/coqlib.cmi tactics/equality.cmi pretyping/evd.cmi \ library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \ @@ -3230,12 +3248,10 @@ contrib/xml/xmlcommand.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \ contrib/xml/xml.cmx contrib/xml/xmlcommand.cmi contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \ parsing/extend.cmi interp/genarg.cmi parsing/pcoq.cmi lib/pp.cmi \ - parsing/pptactic.cmi tactics/tacinterp.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi contrib/xml/xmlcommand.cmi + lib/util.cmi toplevel/vernacinterp.cmi contrib/xml/xmlcommand.cmi contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \ - parsing/pptactic.cmx tactics/tacinterp.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx + lib/util.cmx toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \ ide/utils/configwin_types.cmo ide/utils/configwin.cmi ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \ @@ -112,7 +112,7 @@ PRETYPING=\ pretyping/classops.cmo pretyping/recordops.cmo pretyping/indrec.cmo \ pretyping/evarutil.cmo pretyping/evarconv.cmo \ pretyping/coercion.cmo pretyping/cases.cmo pretyping/pretyping.cmo \ - pretyping/pattern.cmo + pretyping/pattern.cmo pretyping/matching.cmo INTERP=\ interp/topconstr.cmo interp/ppextend.cmo interp/symbols.cmo \ @@ -147,8 +147,7 @@ PROOFS=\ proofs/tacexpr.cmo 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 translate/ppvernacnew.cmo \ - proofs/tactic_debug.cmo + proofs/clenv.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo TACTICS=\ tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ @@ -160,7 +159,8 @@ TACTICS=\ 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 $(TRANSLATE) \ + toplevel/discharge.cmo toplevel/vernacexpr.cmo \ + translate/ppvernacnew.cmo \ toplevel/vernacinterp.cmo toplevel/mltop.cmo \ toplevel/metasyntax.cmo \ toplevel/vernacentries.cmo toplevel/vernac.cmo \ @@ -976,7 +976,7 @@ GRAMMARNEEDEDCMO=\ library/nameops.cmo library/libnames.cmo library/summary.cmo \ library/nametab.cmo library/libobject.cmo library/lib.cmo \ library/goptions.cmo library/decl_kinds.cmo \ - pretyping/rawterm.cmo pretyping/evd.cmo \ + pretyping/rawterm.cmo pretyping/pattern.cmo pretyping/evd.cmo \ interp/topconstr.cmo interp/genarg.cmo \ interp/ppextend.cmo parsing/coqast.cmo parsing/ast.cmo \ proofs/tacexpr.cmo parsing/ast.cmo \ @@ -1051,6 +1051,12 @@ library/nametab.cmo: library/nametab.ml library/nametab.cmx: library/nametab.ml $(OCAMLOPT) -rectypes $(OPTFLAGS) -c $< +proofs/tacexpr.cmo: proofs/tacexpr.ml + $(OCAMLC) -rectypes $(BYTEFLAGS) -c $< + +proofs/tacexpr.cmx: proofs/tacexpr.ml + $(OCAMLOPT) -rectypes $(OPTFLAGS) -c $< + # files compiled with camlp4 because of streams syntax ML4FILES += lib/pp.ml4 \ diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml index ed2896ec90..5c6e845a36 100644 --- a/contrib/correctness/pmlize.ml +++ b/contrib/correctness/pmlize.ml @@ -14,6 +14,7 @@ open Names open Term open Termast open Pattern +open Matching open Pmisc open Ptype diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 9e3e8a1bbb..888f876dee 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -485,8 +485,8 @@ GEXTEND Gram END ;; -let wit_prog, rawwit_prog = Genarg.create_arg "PROGRAMS-PROG" -let wit_typev, rawwit_typev = Genarg.create_arg "PROGRAMS-TYPEV" +let wit_prog, _, rawwit_prog = Genarg.create_arg "PROGRAMS-PROG" +let wit_typev, _, rawwit_typev = Genarg.create_arg "PROGRAMS-TYPEV" open Pp open Util diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml index 5aa497d7f8..eb64b7eb2b 100644 --- a/contrib/correctness/putil.ml +++ b/contrib/correctness/putil.ml @@ -16,6 +16,7 @@ open Nameops open Term open Termops open Pattern +open Matching open Environ open Pmisc diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 0c908e1ad8..c502ea9b01 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -89,38 +89,43 @@ open Extend open Pcoq open Genarg -let wit_minus_div_arg, rawwit_minus_div_arg = Genarg.create_arg "minus_div_arg" -let minus_div_arg = create_generic_entry "minus_div_arg" rawwit_minus_div_arg -let _ = Tacinterp.add_genarg_interp "minus_div_arg" - (fun ist gl x -> - (in_gen wit_minus_div_arg - (out_gen (wit_pair (wit_opt wit_constr) (wit_opt wit_constr)) - (Tacinterp.genarg_interp ist gl - (in_gen (wit_pair (wit_opt rawwit_constr) (wit_opt rawwit_constr)) - (out_gen rawwit_minus_div_arg x)))))) +VERNAC ARGUMENT EXTEND divarg +| [ "div" ":=" constr(adiv) ] -> [ adiv ] +END + +VERNAC ARGUMENT EXTEND minusarg +| [ "minus" ":=" constr(aminus) ] -> [ aminus ] +END +(* +(* The v7->v8 translator needs printers, then temporary use ARGUMENT EXTEND...*) +VERNAC ARGUMENT EXTEND minus_div_arg +| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ] +| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ] +| [ ] -> [ None, None ] +END +*) + +(* For the translator, otherwise the code above is OK *) open Ppconstrnew -let pp_minus_div_arg (omin,odiv) = str "still no printer for minus_div_arg" -let pp_raw_minus_div_arg (omin,odiv) = +let pp_minus_div_arg _prc _prt (omin,odiv) = if omin=None && odiv=None then mt() else spc() ++ str "with" ++ - pr_opt (fun c -> str "minus := " ++ pr_constr c) omin ++ - pr_opt (fun c -> str "div := " ++ pr_constr c) odiv - + pr_opt (fun c -> str "minus := " ++ _prc c) omin ++ + pr_opt (fun c -> str "div := " ++ _prc c) odiv +(* let () = Pptactic.declare_extra_genarg_pprule true - (rawwit_minus_div_arg,pp_raw_minus_div_arg) + (rawwit_minus_div_arg,pp_minus_div_arg) + (globwit_minus_div_arg,pp_minus_div_arg) (wit_minus_div_arg,pp_minus_div_arg) - -open Pcoq.Constr -GEXTEND Gram - GLOBAL: minus_div_arg; - minus_arg: [ [ IDENT "minus"; ":="; aminus = constr -> aminus ] ]; - div_arg: [ [ IDENT "div"; ":="; adiv = constr -> adiv ] ]; - minus_div_arg: - [ [ "with"; m = minus_arg; d = OPT div_arg -> Some m, d - | "with"; d = div_arg; m = OPT minus_arg -> m, Some d - | -> None, None ] ]; +*) +ARGUMENT EXTEND minus_div_arg + TYPED AS constr_opt * constr_opt + PRINTED BY pp_minus_div_arg +| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ] +| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ] +| [ ] -> [ None, None ] END VERNAC COMMAND EXTEND Field diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index ce43da5ded..7d3ed8dd83 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -583,7 +583,7 @@ let blast gls = (* on remplace les ?1 ?2 ... de refine par ? *) parse_tac ((vire_extvar tac_string) ^ ".") - ) + ) else (msgnl (hov 0 (str"Blast failed to prove the goal...")); failwith "echec de blast")) with _ -> failwith "echec de blast" @@ -598,7 +598,8 @@ let blast_tac display_function = function | _ -> failwith "expecting other arguments";; let blast_tac_txt = - blast_tac (function x -> msgnl(Pptactic.pr_raw_tactic x));; + blast_tac + (function x -> msgnl(Pptactic.pr_glob_tactic (Tacinterp.glob_tactic x)));; (* Obsolète ? overwriting_add_tactic "Blast1" blast_tac_txt;; diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 87f8c8af10..78de2fb022 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -367,7 +367,7 @@ let debug_tac2_pcoq tac = (errorlabstrm "DEBUG TACTIC" (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++ fnl () ++ str "the tactic is" ++ fnl () ++ - Pptactic.pr_raw_tactic tac); + Pptactic.pr_glob_tactic tac); result) with e -> @@ -901,11 +901,11 @@ END </cpa> *) TACTIC EXTEND CtDebugTac -| [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq t ] +| [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ] END TACTIC EXTEND CtDebugTac2 -| [ "DebugTac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq t ] +| [ "DebugTac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ] END diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml index 4f03fb06fd..3eb6e7993d 100644 --- a/contrib/interface/dad.ml +++ b/contrib/interface/dad.ml @@ -10,6 +10,7 @@ open Environ;; open Tactics;; open Tacticals;; open Pattern;; +open Matching;; open Reduction;; open Constrextern;; open Constrintern;; diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4 index 343f90d6e5..ca43d00778 100644 --- a/contrib/interface/debug_tac.ml4 +++ b/contrib/interface/debug_tac.ml4 @@ -115,7 +115,7 @@ let count_subgoals2 card_holder := Recursive_fail(List.hd !new_report_holder)); result;; -let rec local_interp : raw_tactic_expr -> report_holder -> tactic = function +let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function (* Node(_, "TACTICLIST", [a;Node(_, "TACLIST", l)]) -> (fun report_holder -> checked_thens report_holder a l) @@ -142,7 +142,7 @@ let rec local_interp : raw_tactic_expr -> report_holder -> tactic = function | t -> (fun report_holder g -> try - let (gls, _) as result = Tacinterp.interp t g in + let (gls, _) as result = Tacinterp.eval_tactic t g in report_holder := (Report_node(true, List.length (sig_it gls), [])) ::!report_holder; result @@ -162,7 +162,7 @@ let rec local_interp : raw_tactic_expr -> report_holder -> tactic = function - In case of success of the first tactic, but count mismatch, then Mismatch n is added to the report holder. *) -and checked_thens: report_holder -> raw_tactic_expr -> raw_tactic_expr list -> tactic = +and checked_thens: report_holder -> glob_tactic_expr -> glob_tactic_expr list -> tactic = (fun report_holder t1 l g -> let flag = ref true in let traceable_t1 = traceable t1 in @@ -174,7 +174,7 @@ and checked_thens: report_holder -> raw_tactic_expr -> raw_tactic_expr list -> t flag (local_interp t1)) else (check_subgoals_count card_holder (List.length l) - flag (Tacinterp.interp t1)) in + flag (Tacinterp.eval_tactic t1)) in let (gls, _) as result = tclTHEN_i tac_t1 (fun i -> @@ -185,7 +185,7 @@ and checked_thens: report_holder -> raw_tactic_expr -> raw_tactic_expr list -> t local_interp tac_i new_holder g else try - let (gls,_) as result = Tacinterp.interp tac_i g in + let (gls,_) as result = Tacinterp.eval_tactic tac_i g in let len = List.length (sig_it gls) in new_holder := (Report_node(true, len, []))::!new_holder; @@ -217,7 +217,7 @@ and checked_thens: report_holder -> raw_tactic_expr -> raw_tactic_expr list -> t reporting information about the success of all tactics in the report holder. It never fails. *) -and checked_then: report_holder -> raw_tactic_expr -> raw_tactic_expr -> tactic = +and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tactic = (fun report_holder t1 t2 g -> let flag = ref true in let card_holder = ref Fail in @@ -225,7 +225,7 @@ and checked_then: report_holder -> raw_tactic_expr -> raw_tactic_expr -> tactic if traceable t1 then (count_subgoals2 card_holder flag (local_interp t1)) else - (count_subgoals card_holder flag (Tacinterp.interp t1)) in + (count_subgoals card_holder flag (Tacinterp.eval_tactic t1)) in let new_tree_holder = ref ([] : report_tree list) in let (gls, _) as result = tclTHEN tac_t1 @@ -235,7 +235,7 @@ and checked_then: report_holder -> raw_tactic_expr -> raw_tactic_expr -> tactic local_interp t2 new_tree_holder g else try - let (gls, _) as result = Tacinterp.interp t2 g in + let (gls, _) as result = Tacinterp.eval_tactic t2 g in new_tree_holder := (Report_node(true, List.length (sig_it gls),[])):: !new_tree_holder; @@ -267,10 +267,10 @@ let on_then = function [t1;t2;l] -> let t1 = out_gen wit_tactic t1 in let t2 = out_gen wit_tactic t2 in let l = out_gen (wit_list0 wit_int) l in - tclTHEN_i (Tacinterp.interp t1) + tclTHEN_i (Tacinterp.eval_tactic t1) (fun i -> if List.mem (i + 1) l then - (Tacinterp.interp t2) + (Tacinterp.eval_tactic t2) else tclIDTAC) | _ -> anomaly "bad arguments for on_then";; @@ -348,7 +348,7 @@ let rec reconstruct_success_tac ast = (str "error in reconstruction with " ++ fnl () ++ (gentacpr ast)));; *) -let rec reconstruct_success_tac tac = +let rec reconstruct_success_tac (tac:glob_tactic_expr) = match tac with TacThens (a,l) -> (function @@ -364,9 +364,9 @@ let rec reconstruct_success_tac tac = | Report_node(false, n, rl) -> let selected_indices = select_success 1 rl in TacAtom (dummy_loc,TacExtend (dummy_loc,"OnThen", - [in_gen rawwit_tactic a; - in_gen rawwit_tactic b; - in_gen (wit_list0 rawwit_int) selected_indices])) + [in_gen globwit_tactic a; + in_gen globwit_tactic b; + in_gen (wit_list0 globwit_int) selected_indices])) | Failed n -> TacId | Tree_fail r -> reconstruct_success_tac a r | _ -> error "this error case should not happen in a THEN tactic") @@ -378,7 +378,7 @@ let rec reconstruct_success_tac tac = errorlabstrm "this error case should not happen on an unknown tactic" (str "error in reconstruction with " ++ fnl () ++ - (pr_raw_tactic tac)));; + (pr_glob_tactic tac)));; let rec path_to_first_error = function @@ -421,7 +421,7 @@ let debug_tac = function msgnl (fnl () ++ str "========= Successful tactic =============" ++ fnl () ++ - pr_raw_tactic compact_success_tac ++ fnl () ++ + pr_glob_tactic compact_success_tac ++ fnl () ++ str "========= End of successful tactic ============"); result) | _ -> error "wrong arguments for debug_tac";; @@ -462,7 +462,7 @@ let rec clean_path tac l = | _, _ -> failwith "this case should not happen in clean_path";; let rec report_error - : raw_tactic_expr -> goal sigma option ref -> raw_tactic_expr ref -> int list ref -> + : glob_tactic_expr -> goal sigma option ref -> glob_tactic_expr ref -> int list ref -> int list -> tactic = fun tac the_goal the_ast returned_path path -> match tac with @@ -523,12 +523,12 @@ let rec report_error if !the_count > 1 then msgnl (str "in branch no " ++ int !the_count ++ - str " after tactic " ++ pr_raw_tactic a); + str " after tactic " ++ pr_glob_tactic a); raise e) | tac -> (fun g -> try - Tacinterp.interp tac g + Tacinterp.eval_tactic tac g with e -> (the_ast := tac; @@ -556,7 +556,7 @@ let descr_first_error tac = fnl () ++ str "on goal" ++ fnl () ++ pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++ str "faulty tactic is" ++ fnl () ++ fnl () ++ - pr_raw_tactic ((*flatten_then*) !the_ast) ++ fnl ()); + pr_glob_tactic ((*flatten_then*) !the_ast) ++ fnl ()); tclIDTAC g)) (* TODO ... used ?? diff --git a/contrib/interface/debug_tac.mli b/contrib/interface/debug_tac.mli index 05cef23aa7..ded714b629 100644 --- a/contrib/interface/debug_tac.mli +++ b/contrib/interface/debug_tac.mli @@ -1,6 +1,6 @@ -val report_error : Tacexpr.raw_tactic_expr -> +val report_error : Tacexpr.glob_tactic_expr -> Proof_type.goal Proof_type.sigma option ref -> - Tacexpr.raw_tactic_expr ref -> int list ref -> int list -> Tacmach.tactic;; + Tacexpr.glob_tactic_expr ref -> int list ref -> int list -> Tacmach.tactic;; -val clean_path : Tacexpr.raw_tactic_expr -> int list -> int list;; +val clean_path : Tacexpr.glob_tactic_expr -> int list -> int list;; diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 9b1602ad41..4abcb5f96f 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -6,6 +6,7 @@ open Tactics;; open Tacticals;; open Hipattern;; open Pattern;; +open Matching;; open Reduction;; open Rawterm;; open Environ;; @@ -17,6 +18,7 @@ open Tacexpr;; open Typing;; open Pp;; open Libnames;; +open Genarg;; open Topconstr;; let zz = (0,0);; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 8191a0978f..1fe718f0e5 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -598,10 +598,6 @@ let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) = CT_coerce_TERM_CHANGE_to_TACTIC_ARG(CT_check_term(xlate_formula c)) | MetaIdArg _ -> xlate_error "MetaIdArg should only be used in quotations" - | MetaNumArg (_,n) -> - CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG - (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT - (CT_coerce_ID_to_ID_OR_INT(CT_metac (CT_int n)))) | t -> CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_call_or_tacarg t) diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 393eff193f..270f09587f 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -109,6 +109,7 @@ open Names open Term open Instantiate open Pattern +open Matching open Tacmach open Tactics open Proof_trees diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4 index 2807a3d6ee..da65de2376 100644 --- a/contrib/xml/xmlentries.ml4 +++ b/contrib/xml/xmlentries.ml4 @@ -32,54 +32,18 @@ open Pcoq;; (* File name *) -let wit_filename, rawwit_filename = Genarg.create_arg "filename" -let filename = Pcoq.create_generic_entry "filename" rawwit_filename -let _ = Tacinterp.add_genarg_interp "filename" - (fun ist gl x -> - (in_gen wit_filename - (out_gen (wit_opt wit_string) - (Tacinterp.genarg_interp ist gl - (in_gen (wit_opt rawwit_string) - (out_gen rawwit_filename x)))))) - -GEXTEND Gram - GLOBAL: filename; - filename: [ [ IDENT "File"; fn = STRING -> Some fn | -> None ] ]; +VERNAC ARGUMENT EXTEND filename +| [ "File" string(fn) ] -> [ Some fn ] +| [ ] -> [ None ] END -let pr_filename = function Some fn -> str " File" ++ str fn | None -> mt () - -let _ = - Pptactic.declare_extra_genarg_pprule true - (rawwit_filename, pr_filename) - (wit_filename, pr_filename) - (* Disk name *) -let wit_diskname, rawwit_diskname = Genarg.create_arg "diskname" -let diskname = create_generic_entry "diskname" rawwit_diskname -let _ = Tacinterp.add_genarg_interp "diskname" - (fun ist gl x -> - (in_gen wit_diskname - (out_gen (wit_opt wit_string) - (Tacinterp.genarg_interp ist gl - (in_gen (wit_opt rawwit_string) - (out_gen rawwit_diskname x)))))) - -GEXTEND Gram - GLOBAL: diskname; - diskname: [ [ IDENT "Disk"; fn = STRING -> Some fn | -> None ] ]; +VERNAC ARGUMENT EXTEND diskname +| [ "Disk" string(fn) ] -> [ Some fn ] +| [ ] -> [ None ] END -open Pp - -let pr_diskname = function Some fn -> str " Disk" ++ str fn | None -> mt () - -let _ = - Pptactic.declare_extra_genarg_pprule true - (rawwit_diskname, pr_diskname) - (wit_diskname, pr_diskname) - VERNAC COMMAND EXTEND Xml | [ "Print" "XML" filename(fn) global(id) ] -> [ Xmlcommand.print id fn ] @@ -95,39 +59,3 @@ VERNAC COMMAND EXTEND Xml [ Xmlcommand.printSection id dn ] *) END -(* -vinterp_add "Print" - (function - [VARG_QUALID id] -> - (fun () -> Xmlcommand.print id None) - | [VARG_QUALID id ; VARG_STRING fn] -> - (fun () -> Xmlcommand.print id (Some fn)) - | _ -> anomaly "This should be trapped");; - -vinterp_add "Show" - (function - [] -> - (fun () -> Xmlcommand.show None) - | [VARG_STRING fn] -> - (fun () -> Xmlcommand.show (Some fn)) - | _ -> anomaly "This should be trapped");; - -vinterp_add "XmlPrintAll" - (function - [] -> (fun () -> Xmlcommand.printAll ()) - | _ -> anomaly "This should be trapped");; - -vinterp_add "XmlPrintModule" - (function - [VARG_QUALID id] -> (fun () -> Xmlcommand.printModule id None) - | [VARG_QUALID id ; VARG_STRING dn] -> - (fun () -> Xmlcommand.printModule id (Some dn)) - | _ -> anomaly "This should be trapped");; - -vinterp_add "XmlPrintSection" - (function - [VARG_IDENTIFIER id] -> (fun () -> Xmlcommand.printSection id None) - | [VARG_IDENTIFIER id ; VARG_STRING dn] -> - (fun () -> Xmlcommand.printSection id (Some dn)) - | _ -> anomaly "This should be trapped");; -*) diff --git a/pretyping/matching.ml b/pretyping/matching.ml new file mode 100644 index 0000000000..caecbf455b --- /dev/null +++ b/pretyping/matching.ml @@ -0,0 +1,250 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(*i*) +open Util +open Names +open Libnames +open Nameops +open Termops +open Reductionops +open Term +open Rawterm +open Environ +open Pattern +(*i*) + +(* Given a term with second-order variables in it, + represented by Meta's, and possibly applied using [SOAPP] to + terms, this function will perform second-order, binding-preserving, + matching, in the case where the pattern is a pattern in the sense + of Dale Miller. + + ALGORITHM: + + Given a pattern, we decompose it, flattening Cast's and apply's, + recursing on all operators, and pushing the name of the binder each + time we descend a binder. + + When we reach a first-order variable, we ask that the corresponding + term's free-rels all be higher than the depth of the current stack. + + When we reach a second-order application, we ask that the + intersection of the free-rels of the term and the current stack be + contained in the arguments of the application, and in that case, we + construct a LAMBDA with the names on the stack. + + *) + +exception PatternMatchingFailure + +let constrain ((n : int),(m : constr)) sigma = + if List.mem_assoc n sigma then + if eq_constr m (List.assoc n sigma) then sigma + else raise PatternMatchingFailure + else + (n,m)::sigma + +let build_lambda toabstract stk (m : constr) = + let rec buildrec m p_0 p_1 = match p_0,p_1 with + | (_, []) -> m + | (n, (na,t)::tl) -> + if List.mem n toabstract then + buildrec (mkLambda (na,t,m)) (n+1) tl + else + buildrec (lift (-1) m) (n+1) tl + in + buildrec m 1 stk + +let memb_metavars m n = + match (m,n) with + | (None, _) -> true + | (Some mvs, n) -> List.mem n mvs + +let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2 + +let matches_core convert allow_partial_app pat c = + let rec sorec stk sigma p t = + let cT = strip_outer_cast t in + match p,kind_of_term cT with + | PSoApp (n,args),m -> + let relargs = + List.map + (function + | PRel n -> n + | _ -> error "Only bound indices are currently allowed in second order pattern matching") + args in + let frels = Intset.elements (free_rels cT) in + if list_subset frels relargs then + constrain (n,build_lambda relargs stk cT) sigma + else + raise PatternMatchingFailure + + | PMeta (Some n), m -> + let depth = List.length stk in + let frels = Intset.elements (free_rels cT) in + if List.for_all (fun i -> i > depth) frels then + constrain (n,lift (-depth) cT) sigma + else + raise PatternMatchingFailure + + | PMeta None, m -> sigma + + | PRef (VarRef v1), Var v2 when v1 = v2 -> sigma + + | PVar v1, Var v2 when v1 = v2 -> sigma + + | PRef ref, _ when constr_of_reference ref = cT -> sigma + + | PRel n1, Rel n2 when n1 = n2 -> sigma + + | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> sigma + + | PSort (RType _), Sort (Type _) -> sigma + + | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app -> + let p = Array.length args2 - Array.length args1 in + if p>=0 then + let args21, args22 = array_chop p args2 in + let sigma = + let depth = List.length stk in + let c = mkApp(c2,args21) in + let frels = Intset.elements (free_rels c) in + if List.for_all (fun i -> i > depth) frels then + constrain (n,lift (-depth) c) sigma + else + raise PatternMatchingFailure in + array_fold_left2 (sorec stk) sigma args1 args22 + else raise PatternMatchingFailure + + | PApp (c1,arg1), App (c2,arg2) -> + (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2 + with Invalid_argument _ -> raise PatternMatchingFailure) + + | PProd (na1,c1,d1), Prod(na2,c2,d2) -> + sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2 + + | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> + sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2 + + | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> + sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2 + + | PRef (ConstRef _ as ref), _ when convert <> None -> + let (env,evars) = out_some convert in + let c = constr_of_reference ref in + if is_conv env evars c cT then sigma + else raise PatternMatchingFailure + + | PCase (_,_,a1,br1), Case (_,_,a2,br2) -> + (* On ne teste pas le prédicat *) + if (Array.length br1) = (Array.length br2) then + array_fold_left2 (sorec stk) (sorec stk sigma a1 a2) br1 br2 + else + raise PatternMatchingFailure + (* À faire *) + | PFix f0, Fix f1 when f0 = f1 -> sigma + | PCoFix c0, CoFix c1 when c0 = c1 -> sigma + | _ -> raise PatternMatchingFailure + + in + Sort.list (fun (a,_) (b,_) -> a<b) (sorec [] [] pat c) + +let matches = matches_core None false + +let pmatches = matches_core None true + +(* To skip to the next occurrence *) +exception NextOccurrence of int + +(* Tells if it is an authorized occurrence *) +let authorized_occ nocc mres = + if nocc = 0 then mres + else raise (NextOccurrence nocc) + +(* Tries to match a subterm of [c] with [pat] *) +let rec sub_match nocc pat c = + match kind_of_term c with + | Cast (c1,c2) -> + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + | PatternMatchingFailure -> + let (lm,lc) = try_sub_match nocc pat [c1] in + (lm,mkCast (List.hd lc, c2)) + | NextOccurrence nocc -> + let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in + (lm,mkCast (List.hd lc, c2))) + | Lambda (x,c1,c2) -> + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + | PatternMatchingFailure -> + let (lm,lc) = try_sub_match nocc pat [c1;c2] in + (lm,mkLambda (x,List.hd lc,List.nth lc 1)) + | NextOccurrence nocc -> + let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in + (lm,mkLambda (x,List.hd lc,List.nth lc 1))) + | Prod (x,c1,c2) -> + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + | PatternMatchingFailure -> + let (lm,lc) = try_sub_match nocc pat [c1;c2] in + (lm,mkProd (x,List.hd lc,List.nth lc 1)) + | NextOccurrence nocc -> + let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in + (lm,mkProd (x,List.hd lc,List.nth lc 1))) + | LetIn (x,c1,t2,c2) -> + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + | PatternMatchingFailure -> + let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in + (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)) + | NextOccurrence nocc -> + let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in + (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))) + | App (c1,lc) -> + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + | PatternMatchingFailure -> + let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in + (lm,mkApp (List.hd le, Array.of_list (List.tl le))) + | NextOccurrence nocc -> + let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in + (lm,mkApp (List.hd le, Array.of_list (List.tl le)))) + | Case (ci,hd,c1,lc) -> + (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + | PatternMatchingFailure -> + let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in + (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) + | NextOccurrence nocc -> + let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in + (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le)))) + | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _ + | Rel _|Meta _|Var _|Sort _ -> + (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with + | PatternMatchingFailure -> raise (NextOccurrence nocc) + | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1))) + +(* Tries [sub_match] for all terms in the list *) +and try_sub_match nocc pat lc = + let rec try_sub_match_rec nocc pat lacc = function + | [] -> raise (NextOccurrence nocc) + | c::tl -> + (try + let (lm,ce) = sub_match nocc pat c in + (lm,lacc@(ce::tl)) + with + | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in + try_sub_match_rec nocc pat [] lc + +let is_matching pat n = + try let _ = matches pat n in true + with PatternMatchingFailure -> false + +let matches_conv env sigma = matches_core (Some (env,sigma)) false + +let is_matching_conv env sigma pat n = + try let _ = matches_conv env sigma pat n in true + with PatternMatchingFailure -> false + diff --git a/pretyping/matching.mli b/pretyping/matching.mli new file mode 100644 index 0000000000..5a789b442e --- /dev/null +++ b/pretyping/matching.mli @@ -0,0 +1,53 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(*i*) +open Names +open Term +open Environ +open Pattern +(*i*) + +(*s This modules implements pattern-matching on terms *) + +exception PatternMatchingFailure + +(* [matches pat c] matches [c] against [pat] and returns the resulting + assignment of metavariables; it raises [PatternMatchingFailure] if + not matchable; bindings are given in increasing order based on the + numbers given in the pattern *) +val matches : + constr_pattern -> constr -> (int * constr) list + +(* [is_matching pat c] just tells if [c] matches against [pat] *) + +val is_matching : + constr_pattern -> constr -> bool + +(* [matches_conv env sigma] matches up to conversion in environment + [(env,sigma)] when constants in pattern are concerned; it raises + [PatternMatchingFailure] if not matchable; bindings are given in + increasing order based on the numbers given in the pattern *) + +val matches_conv : + env -> Evd.evar_map -> constr_pattern -> constr -> (int * constr) list + +(* To skip to the next occurrence *) +exception NextOccurrence of int + +(* Tries to match a subterm of [c] with [pat] *) +val sub_match : + int -> constr_pattern -> constr -> ((int * constr) list * constr) + +(* [is_matching_conv env sigma pat c] tells if [c] matches against [pat] + up to conversion for constants in patterns *) + +val is_matching_conv : + env -> Evd.evar_map -> constr_pattern -> constr -> bool |