aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2003-04-07 17:36:44 +0000
committerherbelin2003-04-07 17:36:44 +0000
commit4ab520180b7597f8358f9d351151cd73e43858a3 (patch)
tree0d8bdd472bedc71ec0bc9bee6f6dd66fde03dba6
parent928287134ab9dd23258c395589f8633e422e939f (diff)
Globalisation des noms de tactiques dans les définitions de tactiques
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3858 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--.depend708
-rw-r--r--Makefile16
-rw-r--r--contrib/correctness/pmlize.ml1
-rw-r--r--contrib/correctness/psyntax.ml44
-rw-r--r--contrib/correctness/putil.ml1
-rw-r--r--contrib/field/field.ml455
-rwxr-xr-xcontrib/interface/blast.ml5
-rw-r--r--contrib/interface/centaur.ml46
-rw-r--r--contrib/interface/dad.ml1
-rw-r--r--contrib/interface/debug_tac.ml440
-rw-r--r--contrib/interface/debug_tac.mli6
-rw-r--r--contrib/interface/pbp.ml2
-rw-r--r--contrib/interface/xlate.ml4
-rw-r--r--contrib/ring/quote.ml1
-rw-r--r--contrib/xml/xmlentries.ml484
-rw-r--r--pretyping/matching.ml250
-rw-r--r--pretyping/matching.mli53
17 files changed, 749 insertions, 488 deletions
diff --git a/.depend b/.depend
index 77437c3450..03bb4245e7 100644
--- a/.depend
+++ b/.depend
@@ -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 \
diff --git a/Makefile b/Makefile
index 00be4061f5..0d48aff515 100644
--- a/Makefile
+++ b/Makefile
@@ -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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 03:36:38 +0000