aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend82
-rw-r--r--.depend.coq80
-rw-r--r--Makefile66
-rw-r--r--lib/util.ml5
-rw-r--r--lib/util.mli1
-rw-r--r--proofs/clenv.ml2
-rw-r--r--proofs/proof_type.mli2
-rw-r--r--proofs/tacinterp.ml128
-rw-r--r--proofs/tacmach.ml1
-rw-r--r--proofs/tacmach.mli1
-rw-r--r--states/MakeInitial.v2
-rw-r--r--tactics/EAuto.v65
-rw-r--r--tactics/eauto.ml293
-rw-r--r--tactics/equality.ml24
14 files changed, 626 insertions, 126 deletions
diff --git a/.depend b/.depend
index 93584a997..5d813ac3e 100644
--- a/.depend
+++ b/.depend
@@ -31,8 +31,6 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi
kernel/univ.cmi: kernel/names.cmi lib/pp.cmi
lib/pp.cmi: lib/pp_control.cmi
-lib/system.cmi: lib/pp.cmi
-lib/util.cmi: lib/pp.cmi
library/declare.cmi: kernel/declarations.cmi kernel/environ.cmi \
kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi
library/global.cmi: kernel/declarations.cmi kernel/environ.cmi \
@@ -48,6 +46,8 @@ library/library.cmi: lib/pp.cmi
library/nametab.cmi: kernel/names.cmi
library/redinfo.cmi: kernel/names.cmi kernel/term.cmi
library/summary.cmi: kernel/names.cmi
+lib/system.cmi: lib/pp.cmi
+lib/util.cmi: lib/pp.cmi
parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
parsing/pcoq.cmi lib/pp.cmi
parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -184,11 +184,11 @@ toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi
toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
kernel/term.cmi
toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi
toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \
toplevel/vernacinterp.cmi
toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
proofs/proof_type.cmi
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi
config/coq_config.cmo: config/coq_config.cmi
config/coq_config.cmx: config/coq_config.cmi
dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi
@@ -313,30 +313,22 @@ lib/dyn.cmo: lib/util.cmi lib/dyn.cmi
lib/dyn.cmx: lib/util.cmx lib/dyn.cmi
lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi
-lib/gmap.cmo: lib/gmap.cmi
-lib/gmap.cmx: lib/gmap.cmi
lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi
lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi
+lib/gmap.cmo: lib/gmap.cmi
+lib/gmap.cmx: lib/gmap.cmi
lib/gset.cmo: lib/gset.cmi
lib/gset.cmx: lib/gset.cmi
lib/hashcons.cmo: lib/hashcons.cmi
lib/hashcons.cmx: lib/hashcons.cmi
lib/options.cmo: lib/util.cmi lib/options.cmi
lib/options.cmx: lib/util.cmx lib/options.cmi
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi
lib/pp_control.cmo: lib/pp_control.cmi
lib/pp_control.cmx: lib/pp_control.cmi
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi
lib/profile.cmo: lib/system.cmi lib/profile.cmi
lib/profile.cmx: lib/system.cmx lib/profile.cmi
-lib/stamps.cmo: lib/stamps.cmi
-lib/stamps.cmx: lib/stamps.cmi
-lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi
-lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
-lib/util.cmo: lib/pp.cmi lib/util.cmi
-lib/util.cmx: lib/pp.cmx lib/util.cmi
library/declare.cmo: kernel/declarations.cmi kernel/environ.cmi \
kernel/evd.cmi kernel/generic.cmi library/global.cmi library/impargs.cmi \
library/indrec.cmi kernel/inductive.cmi library/lib.cmi \
@@ -413,6 +405,14 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
library/summary.cmi
library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
library/summary.cmi
+lib/stamps.cmo: lib/stamps.cmi
+lib/stamps.cmx: lib/stamps.cmi
+lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi
+lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
+lib/util.cmo: lib/pp.cmi lib/util.cmi
+lib/util.cmx: lib/pp.cmx lib/util.cmi
parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi
parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
@@ -805,6 +805,14 @@ tactics/dhyp.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
toplevel/vernacinterp.cmx tactics/dhyp.cmi
tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi
tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi
+tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi kernel/evd.cmi \
+ kernel/generic.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
+ kernel/reduction.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+ tactics/tactics.cmi kernel/term.cmi
+tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx kernel/evd.cmx \
+ kernel/generic.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \
+ kernel/reduction.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+ tactics/tactics.cmx kernel/term.cmx
tactics/elim.cmo: proofs/clenv.cmi kernel/generic.cmi tactics/hiddentac.cmi \
tactics/hipattern.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
proofs/proof_type.cmi kernel/reduction.cmi proofs/tacmach.cmi \
@@ -1075,14 +1083,6 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \
toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi
toplevel/usage.cmo: toplevel/usage.cmi
toplevel/usage.cmx: toplevel/usage.cmi
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
- lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
- library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
- toplevel/vernac.cmi
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
- lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
- library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
- toplevel/vernac.cmi
toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
pretyping/class.cmi toplevel/command.cmi parsing/coqast.cmi \
library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \
@@ -1119,6 +1119,14 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx toplevel/command.cmx \
parsing/coqast.cmx lib/dyn.cmx toplevel/himsg.cmx kernel/names.cmx \
lib/options.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
lib/util.cmx toplevel/vernacinterp.cmi
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
+ lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
+ library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+ toplevel/vernac.cmi
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
+ lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
+ library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+ toplevel/vernac.cmi
contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \
library/declare.cmi kernel/environ.cmi tactics/equality.cmi \
kernel/generic.cmi library/global.cmi kernel/inductive.cmi \
@@ -1135,3 +1143,31 @@ contrib/omega/coq_omega.cmx: parsing/ast.cmx proofs/clenv.cmx \
lib/util.cmx
contrib/omega/omega.cmo: lib/util.cmi
contrib/omega/omega.cmx: lib/util.cmx
+contrib/ring/quote.cmo: library/declare.cmi kernel/generic.cmi \
+ library/global.cmi kernel/instantiate.cmi kernel/names.cmi \
+ proofs/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
+ proofs/proof_type.cmi proofs/tacmach.cmi tactics/tactics.cmi \
+ kernel/term.cmi lib/util.cmi
+contrib/ring/quote.cmx: library/declare.cmx kernel/generic.cmx \
+ library/global.cmx kernel/instantiate.cmx kernel/names.cmx \
+ proofs/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
+ proofs/proof_type.cmx proofs/tacmach.cmx tactics/tactics.cmx \
+ kernel/term.cmx lib/util.cmx
+contrib/ring/ring.cmo: parsing/astterm.cmi kernel/closure.cmi \
+ library/declare.cmi tactics/equality.cmi kernel/evd.cmi \
+ library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \
+ library/lib.cmi library/libobject.cmi kernel/names.cmi proofs/pattern.cmi \
+ lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+ proofs/proof_type.cmi contrib/ring/quote.cmo kernel/reduction.cmi \
+ library/summary.cmi proofs/tacmach.cmi tactics/tactics.cmi \
+ kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
+ toplevel/vernacinterp.cmi
+contrib/ring/ring.cmx: parsing/astterm.cmx kernel/closure.cmx \
+ library/declare.cmx tactics/equality.cmx kernel/evd.cmx \
+ library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \
+ library/lib.cmx library/libobject.cmx kernel/names.cmx proofs/pattern.cmx \
+ lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+ proofs/proof_type.cmx contrib/ring/quote.cmx kernel/reduction.cmx \
+ library/summary.cmx proofs/tacmach.cmx tactics/tactics.cmx \
+ kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
+ toplevel/vernacinterp.cmx
diff --git a/.depend.coq b/.depend.coq
index 0136484fd..88deb93a8 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -1,29 +1,72 @@
-theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo
-theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
-theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo parsing/g_zsyntax.cmo
theories/Zarith/Zmisc.vo: theories/Zarith/Zmisc.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Bool/Bool.vo
-theories/Zarith/ZArith_dec.vo: theories/Zarith/ZArith_dec.v theories/Bool/Sumbool.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo
theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo
+theories/Zarith/ZArith_dec.vo: theories/Zarith/ZArith_dec.v theories/Bool/Sumbool.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo
+theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo
theories/Zarith/Wf_Z.vo: theories/Zarith/Wf_Z.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo
-theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v
+theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
+theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo
+theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v theories/Sets/Relations_1.vo theories/Sets/Relations_2.vo
+theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo
+theories/Sets/Relations_2.vo: theories/Sets/Relations_2.v theories/Sets/Relations_1.vo
+theories/Sets/Relations_2_facts.vo: theories/Sets/Relations_2_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo
+theories/Sets/Relations_1.vo: theories/Sets/Relations_1.v
+theories/Sets/Relations_1_facts.vo: theories/Sets/Relations_1_facts.v theories/Sets/Relations_1.vo
+theories/Sets/Powerset.vo: theories/Sets/Powerset.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
+theories/Sets/Powerset_facts.vo: theories/Sets/Powerset_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo
+theories/Sets/Powerset_Classical_facts.vo: theories/Sets/Powerset_Classical_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo
+theories/Sets/Permut.vo: theories/Sets/Permut.v
+theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo
+theories/Sets/Multiset.vo: theories/Sets/Multiset.v theories/Sets/Permut.vo theories/Arith/Plus.vo
+theories/Sets/Integers.vo: theories/Sets/Integers.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo theories/Sets/Infinite_sets.vo theories/Arith/Compare_dec.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
+theories/Sets/Infinite_sets.vo: theories/Sets/Infinite_sets.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo
+theories/Sets/Image.vo: theories/Sets/Image.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo
+theories/Sets/Finite_sets.vo: theories/Sets/Finite_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo
+theories/Sets/Finite_sets_facts.vo: theories/Sets/Finite_sets_facts.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo
+theories/Sets/Ensembles.vo: theories/Sets/Ensembles.v
+theories/Sets/Cpo.vo: theories/Sets/Cpo.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo
+theories/Sets/Constructive_sets.vo: theories/Sets/Constructive_sets.v theories/Sets/Ensembles.vo
+theories/Sets/Classical_sets.vo: theories/Sets/Classical_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo
+theories/Relations/Rstar.vo: theories/Relations/Rstar.v
+theories/Relations/Relations.vo: theories/Relations/Relations.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo theories/Relations/Operators_Properties.vo
+theories/Relations/Relation_Operators.vo: theories/Relations/Relation_Operators.v theories/Relations/Relation_Definitions.vo theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo
+theories/Relations/Relation_Definitions.vo: theories/Relations/Relation_Definitions.v
+theories/Relations/Operators_Properties.vo: theories/Relations/Operators_Properties.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo
+theories/Relations/Newman.vo: theories/Relations/Newman.v theories/Relations/Rstar.vo
+theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v
+theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Logic/Classical_Prop.vo
+theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
+theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo
+theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rderiv.vo
+theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
+theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo
+theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo theories/Logic/Classical_Prop.vo contrib/omega/Omega.vo
+theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/Zarith/ZArith.vo theories/Reals/TypeSyntax.vo
theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v
+theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v
+theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo
theories/Logic/Classical_Type.vo: theories/Logic/Classical_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v
theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo
theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Prop.vo
-theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo
+theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v theories/Lists/PolyList.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Minus.vo theories/Bool/DecBool.vo
+theories/Lists/Streams.vo: theories/Lists/Streams.v
+theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo
+theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
+theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
+theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
-theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo
theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
+theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo
theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/Wf.vo
theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo
-theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo
+theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
+theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo
theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo
-theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
-theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo
theories/Init/Datatypes.vo: theories/Init/Datatypes.v
+theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo
theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/Bool/Bool.vo
theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v
theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo
@@ -33,8 +76,8 @@ theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo
theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo
theories/Arith/Peano_dec.vo: theories/Arith/Peano_dec.v
theories/Arith/Mult.vo: theories/Arith/Mult.v theories/Arith/Plus.vo theories/Arith/Minus.vo
-theories/Arith/Minus.vo: theories/Arith/Minus.v theories/Arith/Lt.vo theories/Arith/Le.vo
theories/Arith/Min.vo: theories/Arith/Min.v theories/Arith/Arith.vo
+theories/Arith/Minus.vo: theories/Arith/Minus.v theories/Arith/Lt.vo theories/Arith/Le.vo
theories/Arith/Lt.vo: theories/Arith/Lt.v theories/Arith/Le.vo
theories/Arith/Le.vo: theories/Arith/Le.v
theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
@@ -42,19 +85,26 @@ theories/Arith/Even.vo: theories/Arith/Even.v
theories/Arith/Euclid_proof.vo: theories/Arith/Euclid_proof.v theories/Arith/Minus.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
theories/Arith/Euclid_def.vo: theories/Arith/Euclid_def.v theories/Arith/Mult.vo
theories/Arith/EqNat.vo: theories/Arith/EqNat.v
-theories/Arith/Div2.vo: theories/Arith/Div2.v theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Compare_dec.vo theories/Arith/Even.vo
theories/Arith/Div.vo: theories/Arith/Div.v theories/Arith/Le.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo
-theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo
+theories/Arith/Div2.vo: theories/Arith/Div2.v theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Compare_dec.vo theories/Arith/Even.vo
theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
+theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo
theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo parsing/g_natsyntax.cmo
-test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
+test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
+contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/Zarith/ZArith.vo theories/Logic/Eqdep_dec.vo
+contrib/ring/Ring.vo: contrib/ring/Ring.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo contrib/ring/ring.cmo
+contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
+contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
+contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo
+contrib/ring/Quote.vo: contrib/ring/Quote.v contrib/ring/quote.cmo
+contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
contrib/omega/Zpower.vo: contrib/omega/Zpower.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo
contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
-contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo
+contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
tactics/Tauto.vo: tactics/Tauto.v
tactics/Inv.vo: tactics/Inv.v tactics/Equality.vo
tactics/Equality.vo: tactics/Equality.v
diff --git a/Makefile b/Makefile
index 624325fd7..76ebe28ac 100644
--- a/Makefile
+++ b/Makefile
@@ -29,7 +29,7 @@ noargument:
LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
-I proofs -I tactics -I pretyping -I parsing -I toplevel \
- -I contrib/omega
+ -I contrib/omega -I contrib/ring
INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB)
BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG)
@@ -42,9 +42,10 @@ OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
CAMLP4IFDEF=camlp4o pa_ifdef.cmo -D$(OSTYPE)
-COQINCLUDES=-I parsing -I contrib/omega \
+COQINCLUDES=-I parsing -I contrib/omega -I contrib/ring \
-I theories/Init -I theories/Logic -I theories/Arith \
- -I theories/Bool -I theories/Zarith
+ -I theories/Bool -I theories/Zarith -I theories/Lists \
+ -I theories/Sets -I theories/Relations -I theories/Reals
###########################################################################
# Objects files
@@ -111,9 +112,11 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo \
toplevel/usage.cmo toplevel/coqinit.cmo toplevel/coqtop.cmo
HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \
- tactics/tauto.cmo tactics/inv.cmo tactics/leminv.cmo
+ tactics/tauto.cmo tactics/inv.cmo tactics/leminv.cmo \
+ tactics/eauto.cmo
-CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo
+CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
+ contrib/ring/quote.cmo contrib/ring/ring.cmo
CMA=$(CLIBS) $(CAMLP4OBJS)
CMXA=$(CMA:.cma=.cmxa)
@@ -212,7 +215,7 @@ theories/Init/%.vo: theories/Init/%.v states/barestate.coq
init: $(INITVO)
-TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo
+TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo tactics/EAuto.vo
tactics/%.vo: $(COQC)
tactics/%.vo: tactics/%.v states/barestate.coq
@@ -248,7 +251,37 @@ ZARITHVO=theories/Zarith/Wf_Z.vo theories/Zarith/Zsyntax.vo \
theories/Zarith/ZArith_dec.vo theories/Zarith/fast_integer.vo \
theories/Zarith/Zmisc.vo theories/Zarith/zarith_aux.vo
-THEORIESVO = $(LOGICVO) $(ARITHVO) $(BOOLVO) $(ZARITHVO)
+LISTSVO=theories/Lists/List.vo theories/Lists/PolyListSyntax.vo \
+ theories/Lists/ListSet.vo theories/Lists/Streams.vo \
+ theories/Lists/PolyList.vo theories/Lists/TheoryList.vo
+
+SETSVO=theories/Sets/Classical_sets.vo theories/Sets/Permut.vo \
+ theories/Sets/Constructive_sets.vo theories/Sets/Powerset.vo \
+ theories/Sets/Cpo.vo theories/Sets/Powerset_Classical_facts.vo \
+ theories/Sets/Ensembles.vo theories/Sets/Powerset_facts.vo \
+ theories/Sets/Finite_sets.vo theories/Sets/Relations_1.vo \
+ theories/Sets/Finite_sets_facts.vo theories/Sets/Relations_1_facts.vo \
+ theories/Sets/Image.vo theories/Sets/Relations_2.vo \
+ theories/Sets/Infinite_sets.vo theories/Sets/Relations_2_facts.vo \
+ theories/Sets/Integers.vo theories/Sets/Relations_3.vo \
+ theories/Sets/Multiset.vo theories/Sets/Relations_3_facts.vo \
+ theories/Sets/Partial_Order.vo theories/Sets/Uniset.vo
+
+RELATIONSVO=theories/Relations/Newman.vo \
+ theories/Relations/Operators_Properties.vo \
+ theories/Relations/Relation_Definitions.vo \
+ theories/Relations/Relation_Operators.vo \
+ theories/Relations/Relations.vo \
+ theories/Relations/Rstar.vo
+
+REALSVO=theories/Reals/R_Ifp.vo theories/Reals/Reals.vo \
+ theories/Reals/Raxioms.vo theories/Reals/Rfunctions.vo \
+ theories/Reals/Rbase.vo theories/Reals/Rlimit.vo \
+ theories/Reals/Rbasic_fun.vo theories/Reals/TypeSyntax.vo \
+ theories/Reals/Rderiv.vo
+
+THEORIESVO = $(LOGICVO) $(ARITHVO) $(BOOLVO) $(ZARITHVO) $(LISTSVO) \
+ $(SETSVO) $(RELATIONSVO) $(REALSVO)
$(THEORIESVO): states/initial.coq
@@ -258,6 +291,10 @@ logic: $(LOGICVO)
arith: $(ARITHVO)
bool: $(BOOLVO)
zarith: $(ZARITHVO)
+lists: $(LISTSVO)
+sets: $(SETSVO)
+relations: $(RELATIONSVO)
+reals: $(REALSVO)
clean::
rm -f theories/*/*.vo theories/*/*~
@@ -268,13 +305,22 @@ clean::
# contribs
###########################################################################
-CONTRIBVO = contrib/omega/Omega.vo contrib/omega/Zlogarithm.vo \
- contrib/omega/OmegaSyntax.vo contrib/omega/Zpower.vo \
- contrib/omega/Zcomplements.vo
+OMEGAVO = contrib/omega/Omega.vo contrib/omega/Zlogarithm.vo \
+ contrib/omega/OmegaSyntax.vo contrib/omega/Zpower.vo \
+ contrib/omega/Zcomplements.vo
+
+RINGVO = contrib/ring/ArithRing.vo contrib/ring/Ring_normalize.vo \
+ contrib/ring/Ring_theory.vo contrib/ring/Ring.vo \
+ contrib/ring/ZArithRing.vo contrib/ring/Ring_abstract.vo \
+ contrib/ring/Quote.vo
+
+CONTRIBVO = $(OMEGAVO) $(RINGVO)
$(CONTRIBVO): states/initial.coq
contrib: $(CONTRIBVO)
+omega: $(OMEGAVO)
+ring: $(RINGVO)
clean::
rm -f contrib/*/*~ contrib/*/*.cm[io] contrib/*/*.vo
diff --git a/lib/util.ml b/lib/util.ml
index cc2f514a4..e17e586c2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -206,6 +206,11 @@ let list_firstn n l =
in
aux [] (n,l)
+let rec list_last = function
+ | [] -> failwith "list_last"
+ | [x] -> x
+ | _ :: l -> list_last l
+
let list_lastn n l =
let len = List.length l in
let rec aux m l =
diff --git a/lib/util.mli b/lib/util.mli
index 2a8b3ced5..35d181098 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -67,6 +67,7 @@ val list_uniquize : 'a list -> 'a list
val list_subset : 'a list -> 'a list -> bool
val list_splitby : ('a -> bool) -> 'a list -> 'a list * 'a list
val list_firstn : int -> 'a list -> 'a list
+val list_last : 'a list -> 'a
val list_lastn : int -> 'a list -> 'a list
val list_prefix_of : 'a list -> 'a list -> bool
(* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 2ad3f5896..e643f02a4 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -252,7 +252,7 @@ and w_resrec metas evars wc =
| (lhs,(DOP0(Meta k) as rhs))::t -> w_resrec ((k,lhs)::metas) t wc
| (DOPN(Evar evn,_) as evar,rhs)::t ->
- if w_defined_const wc evar then
+ if w_defined_evar wc evn then
let (wc',metas') = w_Unify rhs evar metas wc in
w_resrec metas' t wc'
else
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 9c2ac00ae..a722335d5 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -84,7 +84,7 @@ and tactic = goal sigma -> (goal list sigma * validation)
and validation = (proof_tree list -> proof_tree)
and tactic_arg =
- Command of Coqast.t
+ | Command of Coqast.t
| Constr of constr
| Identifier of identifier
| Integer of int
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 6d999b9c5..af784dcf5 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -24,37 +24,37 @@ let err_msg_tactic_not_found macro_loc macro =
(macro_loc,"macro_expand",
[< 'sTR"Tactic macro ";'sTR macro; 'sPC; 'sTR"not found" >])
-(*Values for interpretation*)
+(* Values for interpretation *)
type value=
- VTactic of tactic
- |VFTactic of tactic_arg list*(tactic_arg list->tactic)
- |VRTactic of (goal list sigma * validation)
- |VArg of tactic_arg
- |VFun of (string*value) list*string option list*Coqast.t
- |VVoid
- |VRec of value ref
-
-(*Gives the identifier corresponding to an Identifier tactic_arg*)
-let id_of_Identifier=function
- Identifier id -> id
+ | VTactic of tactic
+ | VFTactic of tactic_arg list * (tactic_arg list -> tactic)
+ | VRTactic of (goal list sigma * validation)
+ | VArg of tactic_arg
+ | VFun of (string * value) list * string option list * Coqast.t
+ | VVoid
+ | VRec of value ref
+
+(* Gives the identifier corresponding to an Identifier tactic_arg *)
+let id_of_Identifier = function
+ | Identifier id -> id
|_ ->
anomalylabstrm "id_of_IDENTIFIER" [<'sTR "Not an IDENTIFIER tactic_arg">]
-(*Gives the constr corresponding to a Constr tactic_arg*)
+(* Gives the constr corresponding to a Constr tactic_arg *)
let constr_of_Constr=function
Constr c -> c
|_ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a CONSTR tactic_arg">]
-(*Signature for interpretation: val_interp and interpretation functions*)
+(* Signature for interpretation: val_interp and interpretation functions *)
type interp_sign=
evar_declarations*Environ.env*(string*value) list*(int*constr) list*
goal sigma option
-(*Table of interpretation functions*)
+(* Table of interpretation functions *)
let interp_tab=
(Hashtbl.create 17:(string,interp_sign->Coqast.t->value) Hashtbl.t)
-(*Adds an interpretation function*)
+(* Adds an interpretation function *)
let interp_add (ast_typ,interp_fun)=
try
Hashtbl.add interp_tab ast_typ interp_fun
@@ -64,24 +64,24 @@ let interp_add (ast_typ,interp_fun)=
"Cannot add the interpretation function for "; 'sTR ast_typ; 'sTR
" twice">]
-(*Adds a possible existing interpretation function*)
+(* Adds a possible existing interpretation function *)
let overwriting_interp_add (ast_typ,interp_fun)=
if Hashtbl.mem interp_tab ast_typ then
(Hashtbl.remove interp_tab ast_typ;
warning ("Overwriting definition of tactic interpreter command "^ast_typ));
Hashtbl.add interp_tab ast_typ interp_fun
-(*Finds the interpretation function corresponding to a given ast type*)
+(* Finds the interpretation function corresponding to a given ast type *)
let look_for_interp=Hashtbl.find interp_tab
-(*Globalizes the identifier*)
+(* Globalizes the identifier *)
let glob_nvar id=
try
Nametab.sp_of_id CCI id
with
Not_found -> error ("unbound variable "^(string_of_id id))
-(*Summary and Object declaration*)
+(* Summary and Object declaration *)
let mactab=ref Gmap.empty
let lookup id=Gmap.find id !mactab
@@ -104,7 +104,7 @@ let (inMD,outMD)=
open_function=(fun _ -> ());
specification_function=(fun x -> x)})
-(*Adds a Tactic Definition in the table*)
+(* Adds a Tactic Definition in the table *)
let add_tacdef na vbody =
if Gmap.mem na !mactab then
errorlabstrm "Tacdef.add_tacdef"
@@ -112,22 +112,22 @@ let add_tacdef na vbody =
let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in
if Options.is_verbose() then mSGNL [< 'sTR (na^" is defined") >]
-(*Unboxes the tactic_arg*)
+(* Unboxes the tactic_arg *)
let unvarg=function
VArg a -> a
|_ -> errorlabstrm "unvarg" [<'sTR "Not a tactic argument">]
-(*Unboxes VRec*)
+(* Unboxes VRec *)
let unrec=function
VRec v -> !v
|a -> a
-(*Unboxes REDEXP*)
+(* Unboxes REDEXP *)
let unredexp=function
Redexp c -> c
|_ -> errorlabstrm "unredexp" [<'sTR "Not a REDEXP tactic_arg">]
-(*Reads the head of Fun*)
+(* Reads the head of Fun *)
let read_fun ast=
let rec read_fun_rec=function
Node(_,"VOID",[])::tl -> None::(read_fun_rec tl)
@@ -141,7 +141,7 @@ let read_fun ast=
|_ ->
anomalylabstrm "Tacinterp.read_fun" [<'sTR "Fun not well formed">]
-(*Reads the clauses of a Rec*)
+(* Reads the clauses of a Rec *)
let rec read_rec_clauses=function
[] -> []
|Node(_,"RECCLAUSE",[Nvar(_,name);it;body])::tl ->
@@ -150,8 +150,8 @@ let rec read_rec_clauses=function
anomalylabstrm "Tacinterp.read_rec_clauses" [<'sTR
"Rec not well formed">]
-(*Associates variables with values and gives the remaining variables and
- values*)
+(* Associates variables with values and gives the remaining variables and
+ values *)
let head_with_value (lvar,lval)=
let rec head_with_value_rec lacc=function
([],[]) -> (lacc,[],[])
@@ -164,24 +164,24 @@ let head_with_value (lvar,lval)=
in
head_with_value_rec [] (lvar,lval)
-(*Type of hypotheses for a Match Context rule*)
+(* Type of hypotheses for a Match Context rule *)
type match_context_hyps=
NoHypId of constr_pattern
|Hyp of string*constr_pattern
-(*Type of a Match rule for Match Context and Match*)
+(* Type of a Match rule for Match Context and Match *)
type match_rule=
Pat of match_context_hyps list*constr_pattern*Coqast.t
|All of Coqast.t
-(*Gives the ast of a COMMAND ast node*)
+(* Gives the ast of a COMMAND ast node *)
let ast_of_command=function
Node(_,"COMMAND",[c]) -> c
|ast ->
anomaly_loc (Ast.loc ast, "Tacinterp.ast_of_command",[<'sTR
"Not a COMMAND ast node: ";print_ast ast>])
-(*Reads the hypotheses of a Match Context rule*)
+(* Reads the hypotheses of a Match Context rule *)
let rec read_match_context_hyps evc env=function
Node(_,"MATCHCONTEXTHYPS",[pc])::tl ->
(NoHypId (snd (interp_constrpattern evc env (ast_of_command
@@ -194,7 +194,7 @@ let rec read_match_context_hyps evc env=function
"Not a MATCHCONTEXTHYP ast node: ";print_ast ast>])
|[] -> []
-(*Reads the rules of a Match Context*)
+(* Reads the rules of a Match Context *)
let rec read_match_context_rule evc env=function
Node(_,"MATCHCONTEXTRULE",[tc])::tl ->
(All tc)::(read_match_context_rule evc env tl)
@@ -209,7 +209,7 @@ let rec read_match_context_rule evc env=function
"Not a MATCHCONTEXTRULE ast node: ";print_ast ast>])
|[] -> []
-(*Reads the rules of a Match*)
+(* Reads the rules of a Match *)
let rec read_match_rule evc env=function
Node(_,"MATCHRULE",[te])::tl ->
(All te)::(read_match_rule evc env tl)
@@ -221,18 +221,18 @@ let rec read_match_rule evc env=function
"Not a MATCHRULE ast node: ";print_ast ast>])
|[] -> []
-(*Transforms a type_judgment signature into a (string*constr) list*)
+(* Transforms a type_judgment signature into a (string*constr) list *)
let make_hyps hyps=
let lid=List.map string_of_id (ids_of_sign hyps)
and lhyp=List.map body_of_type (vals_of_sign hyps)
in
List.combine lid lhyp
-(*For Match Context and Match*)
+(* For Match Context and Match *)
exception No_match
exception Not_coherent_metas
-(*Verifies if the matched list is coherent with respect to lcm*)
+(* Verifies if the matched list is coherent with respect to lcm *)
let rec verify_metas_coherence lcm=function
(num,csr)::tl ->
if (List.for_all
@@ -246,14 +246,14 @@ let rec verify_metas_coherence lcm=function
raise Not_coherent_metas
|[] -> []
-(*Tries to match a pattern and a constr*)
+(* Tries to match a pattern and a constr *)
let apply_matching pat csr=
try
(Pattern.matches pat csr)
with
PatternMatchingFailure -> raise No_match
-(*Tries to match one hypothesis with a list of hypothesis patterns*)
+(* Tries to match one hypothesis with a list of hypothesis patterns *)
let apply_one_hyp_context lmatch mhyps (idhyp,hyp)=
let rec apply_one_hyp_context_rec (idhyp,hyp) mhyps_acc=function
(Hyp (idpat,pat))::tl ->
@@ -277,7 +277,7 @@ let apply_one_hyp_context lmatch mhyps (idhyp,hyp)=
in
apply_one_hyp_context_rec (idhyp,hyp) [] mhyps
-(*Prepares the lfun list for constr substitutions*)
+(* Prepares the lfun list for constr substitutions *)
let rec make_subs_list=function
(id,VArg (Identifier i))::tl ->
(id_of_string id,VAR i)::(make_subs_list tl)
@@ -286,11 +286,11 @@ let rec make_subs_list=function
|e::tl -> make_subs_list tl
|[] -> []
-(*Interprets any expression*)
+(* Interprets any expression *)
let rec val_interp (evc,env,lfun,lmatch,goalopt) ast=
-(* mSGNL [<print_ast ast>];*)
+(* mSGNL [<print_ast ast>]; *)
-(*mSGNL [<print_ast (Termast.bdize false (Pretty.assumptions_for_print []) ((reduction_of_redexp redexp) env evc c))>];*)
+(* mSGNL [<print_ast (Termast.bdize false (Pretty.assumptions_for_print []) ((reduction_of_redexp redexp) env evc c))>]; *)
match ast with
Node(_,"APP",l) ->
@@ -358,12 +358,12 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt) ast=
VArg (Clause (List.map (fun ast -> id_of_Identifier (unvarg (val_interp
(evc,env,lfun,lmatch,goalopt) ast))) cl))
|Node(_,"TACTIC",[ast]) -> VArg (Tac (tac_interp lfun lmatch ast))
-(*Remains to treat*)
+(* Remains to treat *)
|Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) ->
VArg ((Fixexp (id_of_string s,n,c)))
|Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) ->
VArg ((Cofixexp (id_of_string s,c)))
-(*End of Remains to treat*)
+(* End of Remains to treat *)
|Node(_,"INTROPATTERN", [ast]) ->
VArg ((Intropattern (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)
ast)))
@@ -380,7 +380,7 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt) ast=
|_ ->
anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",[<'sTR
"Unrecognizable ast: ";print_ast ast>])
-(*Interprets an application node*)
+(* Interprets an application node *)
and app_interp evc env lfun lmatch goalopt fv largs ast=
match fv with
VFTactic(l,f) -> VFTactic(l@(List.map unvarg largs),f)
@@ -398,7 +398,7 @@ and app_interp evc env lfun lmatch goalopt fv largs ast=
|_ ->
anomaly_loc (Ast.loc ast, "Tacinterp.app_interp",[<'sTR
"Illegal application: "; print_ast ast>])
-(*Interprets recursive expressions*)
+(* Interprets recursive expressions *)
and rec_interp evc env lfun lmatch goalopt ast=function
[Node(_,"RECCLAUSE",_)] as l ->
let (name,var,body)=List.hd (read_rec_clauses l)
@@ -427,7 +427,7 @@ and rec_interp evc env lfun lmatch goalopt ast=function
|_ ->
anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",[<'sTR
"Rec not well formed: "; print_ast ast>])
-(*Interprets the clauses of a let*)
+(* Interprets the clauses of a let *)
and let_interp evc env lfun lmatch goalopt ast=function
[] -> []
|Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl ->
@@ -436,7 +436,7 @@ and let_interp evc env lfun lmatch goalopt ast=function
|_ ->
anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",[<'sTR
"Let not well formed: "; print_ast ast>])
-(*Interprets the Match Context expressions*)
+(* Interprets the Match Context expressions *)
and match_context_interp evc env lfun lmatch goalopt ast lmr=
let rec apply_match_context evc env lfun lmatch goalopt=function
(All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t
@@ -466,7 +466,7 @@ and match_context_interp evc env lfun lmatch goalopt ast lmr=
in
apply_match_context evc env lfun lmatch goalopt (read_match_context_rule
evc env lmr)
-(*Tries to match the hypotheses in a Match Context*)
+(* Tries to match the hypotheses in a Match Context *)
and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps
hyps=
let rec apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun
@@ -494,7 +494,7 @@ and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps
in
apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt [] lgmatch
mhyps hyps []
-(*Interprets the Match expressions*)
+(* Interprets the Match expressions *)
and match_interp evc env lfun lmatch goalopt ast lmr=
let rec apply_match evc env lfun lmatch goalopt csr=function
(All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t
@@ -516,7 +516,7 @@ and match_interp evc env lfun lmatch goalopt ast lmr=
and ilr=read_match_rule evc env (List.tl lmr)
in
apply_match evc env lfun lmatch goalopt csr ilr
-(*Interprets tactic expressions*)
+(* Interprets tactic expressions *)
and tac_interp lfun lmatch ast g=
let evc=project g
and env=pf_env g
@@ -528,9 +528,9 @@ and tac_interp lfun lmatch ast g=
|_ ->
errorlabstrm "Tacinterp.interp_rec" [<'sTR
"Interpretation gives a non-tactic value">]
-(*Interprets a primitive tactic*)
+(* Interprets a primitive tactic *)
and interp_atomic loc opn args=vernac_tactic(opn,args)
-(*Interprets sequences of tactics*)
+(* Interprets sequences of tactics *)
and interp_semi_list acc lfun lmatch=function
(Node(_,"TACLIST",seq))::l ->
interp_semi_list (tclTHENS acc (List.map (tac_interp lfun lmatch) seq))
@@ -538,7 +538,7 @@ and interp_semi_list acc lfun lmatch=function
|t::l ->
interp_semi_list (tclTHEN acc (tac_interp lfun lmatch t)) lfun lmatch l
|[] -> acc
-(*Interprets bindings for tactics*)
+(* Interprets bindings for tactics *)
and bind_interp evc env lfun lmatch goalopt=function
Node(_,"BINDING", [Num(_,n);Node(loc,"COMMAND",[c])]) ->
(NoDep n,constr_of_Constr (unvarg (val_interp
@@ -553,7 +553,7 @@ and bind_interp evc env lfun lmatch goalopt=function
|x ->
errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding";
print_ast x>]
-(*Interprets a COMMAND expression*)
+(* Interprets a COMMAND expression *)
and com_interp (evc,env,lfun,lmatch,goalopt)=function
Node(_,"EVAL",[c;rtc]) ->
let redexp=
@@ -562,7 +562,7 @@ and com_interp (evc,env,lfun,lmatch,goalopt)=function
VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr1 evc
env (make_subs_list lfun) lmatch c)))
|c -> VArg (Constr (interp_constr1 evc env (make_subs_list lfun) lmatch c))
-(*Interprets a CASTEDCOMMAND expression*)
+(* Interprets a CASTEDCOMMAND expression *)
and cast_com_interp (evc,env,lfun,lmatch,goalopt) com=
match goalopt with
Some gl ->
@@ -595,12 +595,12 @@ and cvt_unfold (evc,env,lfun,lmatch,goalopt)=function
(List.map num_of_ast nums,glob_nvar (id_of_Identifier (unvarg (val_interp
(evc,env,lfun,lmatch,goalopt) com))))
|arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold")
-(*Interprets the arguments of Fold*)
+(* Interprets the arguments of Fold *)
and cvt_fold (evc,env,lfun,lmatch,goalopt)=function
Node(_,"COMMAND",[c]) as ast ->
constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) ast))
|arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold")
-(*Interprets the reduction flags*)
+(* Interprets the reduction flags *)
and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf=
let beta = ref false in
let delta = ref false in
@@ -651,7 +651,7 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf=
(false,_) -> (fun _ -> false)
| (true,None) -> (fun _ -> true)
| (true,Some p) -> p }
-(*Interprets a reduction expression*)
+(* Interprets a reduction expression *)
and redexp_of_ast (evc,env,lfun,lmatch,goalopt)=function
|("Red", []) -> Red
|("Hnf", []) -> Hnf
@@ -664,7 +664,7 @@ and redexp_of_ast (evc,env,lfun,lmatch,goalopt)=function
|("Pattern",lp) ->
Pattern (List.map (cvt_pattern (evc,env,lfun,lmatch,goalopt)) lp)
|(s,_) -> invalid_arg ("malformed reduction-expression: "^s)
-(*Interprets the patterns of Intro*)
+(* Interprets the patterns of Intro *)
and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)=function
Node(_,"IDENTIFIER", [Nvar(loc,s)]) ->
IdPat (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
@@ -679,7 +679,7 @@ and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)=function
errorlabstrm "cvt_intro_pattern"
[<'sTR "Not the expected form for an introduction pattern!";print_ast
x>]
-(*Interprets a pattern of Let*)
+(* Interprets a pattern of Let *)
and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l)=function
Node(_,"HYPPATTERN", Nvar(loc,s)::nums) ->
(o,(id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
@@ -691,10 +691,10 @@ and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l)=function
(Some (List.map num_of_ast nums), l)
|arg -> invalid_arg_loc (Ast.loc arg,"cvt_hyppattern")
-(*Interprets tactic arguments*)
+(* Interprets tactic arguments *)
let interp_tacarg sign ast=unvarg (val_interp sign ast)
-(*Initial call for interpretation*)
+(* Initial call for interpretation *)
let interp=tac_interp [] []
let is_just_undef_macro ast =
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 350b3c1db..ac4287ecb 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -173,6 +173,7 @@ let w_add_sign = w_add_sign
let ctxt_type_of = ctxt_type_of
let w_defined_const wc k = defined_constant (w_env wc) k
+let w_defined_evar wc k = Evd.is_defined (w_Underlying wc) k
let w_const_value wc = constant_value (w_env wc)
let w_conv_x wc m n = is_conv (w_env wc) (w_Underlying wc) m n
let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index b27b0b789..0fb2caa34 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -201,6 +201,7 @@ val w_hnf_constr : walking_constraints -> constr -> constr
val w_conv_x : walking_constraints -> constr -> constr -> bool
val w_const_value : walking_constraints -> constr -> constr
val w_defined_const : walking_constraints -> constr -> bool
+val w_defined_evar : walking_constraints -> int -> bool
(*s Tactic Registration. *)
diff --git a/states/MakeInitial.v b/states/MakeInitial.v
index 7acdf7c1b..eae6c4159 100644
--- a/states/MakeInitial.v
+++ b/states/MakeInitial.v
@@ -4,3 +4,5 @@ Require Export Logic_TypeSyntax.
Require Export Equality.
Require Export Tauto.
Require Export Inv.
+Require Export EAuto.
+
diff --git a/tactics/EAuto.v b/tactics/EAuto.v
new file mode 100644
index 000000000..76b993b21
--- /dev/null
+++ b/tactics/EAuto.v
@@ -0,0 +1,65 @@
+(****************************************************************************)
+(* The Calculus of Inductive Constructions *)
+(* *)
+(* Projet Coq *)
+(* *)
+(* INRIA LRI-CNRS ENS-CNRS *)
+(* Rocquencourt Orsay Lyon *)
+(* *)
+(* Coq V6.3 *)
+(* July 1st 1999 *)
+(* *)
+(****************************************************************************)
+(* Prolog.v *)
+(****************************************************************************)
+
+Grammar tactic simple_tactic :=
+ eapply [ "EApply" com_binding_list($cl) ]
+ -> [(EApplyWithBindings ($LIST $cl))]
+| eexact [ "EExact" constrarg($c) ] -> [(EExact $c)]
+| prolog [ "Prolog" "[" constrarg_list($l) "]" numarg($n) ]
+ -> [(Prolog $n ($LIST $l))]
+| instantiate [ "Instantiate" numarg($n) constrarg($c) ]
+ -> [(Instantiate $n $c)]
+| normevars [ "NormEvars" ] -> [(NormEvars)]
+| etrivial [ "ETrivial" ] -> [(ETrivial)]
+| eauto [ "EAuto" ] -> [(EAuto)]
+| eauto_n [ "EAuto" numarg($n) ] -> [(EAuto $n)]
+| eauto_with [ "EAuto" "with" ne_identarg_list($lid) ]
+ -> [(EAuto ($LIST $lid))]
+| eauto_n_with [ "EAuto" numarg($n) "with" ne_identarg_list($lid) ]
+ -> [(EAuto $n ($LIST $lid))]
+| eauto_with_star [ "EAuto" "with" "*" ]
+ -> [(EAuto "*")]
+| eauto_n_with_star [ "EAuto" numarg($n) "with" "*" ]
+ -> [(EAuto $n "*")].
+
+Syntax tactic level 0:
+ eauto_with [(EAuto ($LIST $lid))] ->
+ [ "EAuto" [1 0] "with " [<hov 0> (LISTSPC ($LIST $lid))] ]
+| eauto [(EAuto)] -> ["EAuto"]
+| eauto_n_with [(EAuto ($NUM $n) ($LIST $lid))] ->
+ [ "EAuto " $n [1 0] "with " [<hov 0> (LISTSPC ($LIST $lid))] ]
+| eauto_n [(EAuto ($NUM $n))] -> ["EAuto " $n]
+| eauto_with_star [(EAuto "*")] ->
+ [ "EAuto with *" ]
+| eauto_n_with_star [(EAuto ($NUM $n) "*")] ->
+ [ "EAuto " $n " with *" ]
+| etrivial [(ETrivial)] -> ["ETrivial"]
+
+| eexact [(EExact $c)] -> ["EExact " $c]
+
+| eapply [(EApplyWithBindings $c ($LIST $bl))]
+ -> ["EApply " $c (WITHBINDING ($LIST $bl))]
+
+| prolog [(Prolog ($NUM $n) ($LIST $l))]
+ -> [ [<hov 0> "Prolog" [1 2] "[" [<hov 0> (LISTSPC ($LIST $l)) ] "]"
+ [1 2] $n] ]
+
+| instantiate [(Instantiate ($NUM $n) $c)] -> ["Instantiate " $n [1 2] $c]
+
+| normevars [(NormEvars)] -> ["NormEvars"].
+
+
+(* $Id$ *)
+
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
new file mode 100644
index 000000000..69d4e59c6
--- /dev/null
+++ b/tactics/eauto.ml
@@ -0,0 +1,293 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Sign
+open Reduction
+open Proof_type
+open Proof_trees
+open Tacmach
+open Tactics
+open Pattern
+open Clenv
+open Auto
+
+let e_give_exact c gl =
+ tclTHEN (unify (pf_type_of gl c)) (Tactics.exact c) gl
+
+let assumption id = e_give_exact (VAR id)
+
+let e_assumption gl =
+ tclFIRST (List.map assumption (ids_of_sign (pf_untyped_hyps gl))) gl
+
+let e_give_exact_constr = hide_constr_tactic "EExact" e_give_exact
+
+let registered_e_assumption gl =
+ tclFIRST (List.map (fun id gl -> e_give_exact_constr (VAR id) gl)
+ (ids_of_sign (pf_untyped_hyps gl))) gl
+
+let e_resolve_with_bindings_tac (c,lbind) gl =
+ let (wc,kONT) = startWalk gl in
+ let t = w_hnf_constr wc (w_type_of wc c) in
+ let clause = make_clenv_binding_apply wc (c,t) lbind in
+ e_res_pf kONT clause gl
+
+let e_resolve_with_bindings =
+ tactic_com_bind_list e_resolve_with_bindings_tac
+
+let vernac_e_resolve_with_bindings =
+ hide_cbindl_tactic "EApplyWithBindings" e_resolve_with_bindings_tac
+
+let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,[]) gls
+let resolve_constr c gls = Tactics.apply_with_bindings (c,[]) gls
+
+let vernac_e_resolve_constr =
+ hide_constr_tactic "EApply" e_resolve_constr
+
+(************************************************************************)
+(* PROLOG tactic *)
+(************************************************************************)
+
+let one_step l gl =
+ [Tactics.intro]
+ @ (List.map e_resolve_constr (List.map (fun x -> VAR x)
+ (ids_of_sign (pf_untyped_hyps gl))))
+ @ (List.map e_resolve_constr l)
+ @ (List.map assumption (ids_of_sign (pf_untyped_hyps gl)))
+
+let rec prolog l n gl =
+ if n <= 0 then error "prolog - failure";
+ let prol = (prolog l (n-1)) in
+ (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
+
+let prolog_tac lcom n gl =
+ let l = List.map (pf_interp_constr gl) lcom in
+ try (prolog l n gl)
+ with UserError ("Refiner.tclFIRST",_) ->
+ errorlabstrm "Prolog.prolog" [< 'sTR "Prolog failed" >]
+
+let evars_of evc c =
+ let rec evrec acc = function
+ | DOPN(Evar n,_) as k when Evd.in_dom evc n -> k :: acc
+ | DOPN(_,cl) -> Array.fold_right (fun c acc -> evrec acc c) cl acc
+ | DOP2(_,c1,c2) -> evrec (evrec acc c2) c1
+ | DOP1(_,c) -> evrec acc c
+ | DLAM(_,c) -> evrec acc c
+ | DLAMV(_,cl) -> Array.fold_right (fun c acc -> evrec acc c) cl acc
+ | _ -> acc
+ in
+ List.rev (evrec [] c)
+
+let instantiate n c gl =
+ let sigma = project gl in
+ let evl = evars_of sigma (pf_concl gl) in
+ let (wc,kONT) = startWalk gl in
+ if List.length evl < n then error "not enough evars";
+ let (n,_) as k = destEvar (List.nth evl (n-1)) in
+ if Evd.is_defined sigma n then
+ error "Instantiate called on already-defined evar";
+ let wc' = w_Define n c wc in
+ kONT wc' gl
+
+let instantiate_tac = function
+ | [Integer n; Command com] ->
+ (fun gl -> instantiate n (pf_interp_constr gl com) gl)
+ | _ -> invalid_arg "Instantiate called with bad arguments"
+
+let whd_evar env sigma = function
+ | DOPN(Evar n, cl) as k ->
+ if Evd.in_dom sigma n & Evd.is_defined sigma n then
+ Instantiate.existential_value sigma (n,cl)
+ else
+ k
+ | x -> x
+
+let normEvars gl =
+ let sigma = project gl in
+ let env = pf_env gl in
+ let nf_evar = strong whd_evar
+ and simplify = nf_betaiota in
+ convert_concl (nf_evar env sigma (simplify env sigma (pf_concl gl))) gl
+
+let vernac_prolog =
+ let uncom = function
+ | Command com -> com
+ | _ -> assert false
+ in
+ let gentac =
+ hide_tactic "Prolog"
+ (function
+ | (Integer n) :: al -> prolog_tac (List.map uncom al) n
+ | _ -> assert false)
+ in
+ fun coms n ->
+ gentac ((Integer n) :: (List.map (fun com -> (Command com)) coms))
+
+let vernac_instantiate =
+ let gentac = hide_tactic "Instantiate" instantiate_tac in
+ fun n com -> gentac [Integer n; Command com]
+
+let vernac_normevars =
+ hide_atomic_tactic "NormEvars" normEvars
+
+open Auto
+
+(***************************************************************************)
+(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
+(***************************************************************************)
+
+(* A registered version of tactics in order to keep a trace *)
+
+let unify_e_resolve (c,clenv) gls =
+ let (wc,kONT) = startWalk gls in
+ let clenv' = connect_clenv wc clenv in
+ let _ = clenv_unique_resolver false clenv' gls in
+ vernac_e_resolve_constr c gls
+
+let rec e_trivial_fail_db db_list local_db goal =
+ let tacl =
+ registered_e_assumption ::
+ (tclTHEN Tactics.intro
+ (function g'->
+ let (hn,htyp) = hd_sign (pf_untyped_hyps g') in
+ let hintl = make_resolve_hyp hn htyp in
+ (e_trivial_fail_db db_list
+ (Hint_db.add_list hintl local_db) g'))) ::
+ (e_trivial_resolve db_list local_db (pf_concl goal))
+ in
+ tclFIRST (List.map tclCOMPLETE tacl) goal
+
+and e_my_find_search db_list local_db hdc concl =
+ let hdc = head_of_constr_reference hdc in
+ let hintl =
+ if occur_existential concl then
+ list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list)
+ else
+ list_map_append (fun db -> Hint_db.map_auto (hdc,concl) db)
+ (local_db::db_list)
+ in
+ let tac_of_hint =
+ fun ({pri=b; pat = p; code=t} as patac) ->
+ (b,
+ match t with
+ | Res_pf (term,cl) -> unify_resolve (term,cl)
+ | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
+ | Give_exact (c) -> e_give_exact_constr c
+ | Res_pf_THEN_trivial_fail (term,cl) ->
+ tclTHEN (unify_e_resolve (term,cl))
+ (e_trivial_fail_db db_list local_db)
+ | Unfold_nth c -> unfold_constr c
+ | Extern tacast -> Tacticals.conclPattern concl
+ (out_some p) tacast)
+ in
+ List.map tac_of_hint hintl
+
+and e_trivial_resolve db_list local_db gl =
+ try
+ Auto.priority
+ (e_my_find_search db_list local_db
+ (List.hd (head_constr_bound gl [])) gl)
+ with Bound | Not_found -> []
+
+(***
+let vernac_e_trivial
+ = hide_atomic_tactic "ETrivial" e_trivial_fail
+****)
+
+let e_possible_resolve db_list local_db gl =
+ try List.map snd (e_my_find_search db_list local_db
+ (List.hd (head_constr_bound gl [])) gl)
+ with Bound | Not_found -> []
+
+(* A version with correct (?) backtracking using operations on lists
+ of goals *)
+
+let assumption_tac_list id = apply_tac_list (e_give_exact_constr (VAR id))
+
+exception Nogoals
+
+let find_first_goal gls =
+ try first_goal gls with UserError _ -> raise Nogoals
+
+let rec e_search n db_list local_db lg =
+ try
+ let g = find_first_goal lg in
+ if n = 0 then error "BOUND 2";
+ let assumption_tacs =
+ List.map
+ (fun id gls ->
+ then_tactic_list
+ (assumption_tac_list id)
+ (e_search n db_list local_db)
+ gls)
+ (ids_of_sign (pf_untyped_hyps g))
+ in
+ let intro_tac =
+ apply_tac_list
+ (tclTHEN Tactics.intro
+ (fun g' ->
+ let (hid,htyp) = hd_sign (pf_untyped_hyps g') in
+ let hintl = make_resolve_hyp hid htyp in
+ (tactic_list_tactic
+ (e_search n db_list
+ (Hint_db.add_list hintl local_db))) g'))
+ in
+ let rec_tacs =
+ List.map
+ (fun ntac lg' ->
+ (then_tactic_list
+ (apply_tac_list ntac)
+ (e_search (n-1) db_list local_db) lg'))
+ (e_possible_resolve db_list local_db (pf_concl g))
+ in
+ tclFIRSTLIST (assumption_tacs @ (intro_tac :: rec_tacs)) lg
+ with Nogoals ->
+ tclIDTAC_list lg
+
+let e_search_auto n db_list gl =
+ tactic_list_tactic
+ (e_search n db_list (make_local_hint_db (pf_untyped_hyps gl)))
+ gl
+
+let eauto n dbnames =
+ let db_list =
+ List.map
+ (fun x ->
+ try Stringmap.find x !searchtable
+ with Not_found -> error ("EAuto: "^x^": No such Hint database"))
+ ("core"::dbnames)
+ in
+ tclTRY (tclCOMPLETE (e_search_auto n db_list))
+
+let default_eauto gl = eauto !default_search_depth [] gl
+
+let full_eauto n gl =
+ let dbnames = stringmap_dom !searchtable in
+ let dbnames = list_subtract dbnames ["v62"] in
+ let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
+ let local_db = make_local_hint_db (pf_untyped_hyps gl) in
+ tclTRY (tclCOMPLETE (e_search_auto n db_list)) gl
+
+let default_full_auto gl = full_auto !default_search_depth gl
+
+let dyn_eauto l = match l with
+ | [] -> default_eauto
+ | [Integer n] -> eauto n []
+ | [Quoted_string "*"] -> default_full_auto
+ | [Integer n; Quoted_string "*"] -> full_eauto n
+ | (Integer n) :: l1 ->
+ eauto n (List.map
+ (function
+ | Identifier id -> (string_of_id id)
+ | _ -> bad_tactic_args "dyn_eauto" l) l1)
+ | _ ->
+ eauto !default_search_depth
+ (List.map
+ (function Identifier id -> (string_of_id id)
+ | _ -> bad_tactic_args "dyn_eauto" l) l)
+
+let h_eauto = hide_tactic "EAuto" dyn_eauto
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 95d61b4cf..3fac4eb2f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -200,12 +200,12 @@ let eq_pattern () = get_pat eq_pattern_mark
let not_pattern () = get_pat not_pattern_mark
let imp_False_pattern () = get_pat imp_False_pattern_mark
-let eq= { eq = put_squel mmk "eq";
- ind = put_squel mmk "eq_ind" ;
- rrec = Some (put_squel mmk "eq_rec");
- rect = Some (put_squel mmk "eq_rect");
- congr = put_squel mmk "f_equal" ;
- sym = put_squel mmk "sym_eq" }
+let eq = { eq = put_squel mmk "eq";
+ ind = put_squel mmk "eq_ind" ;
+ rrec = Some (put_squel mmk "eq_rec");
+ rect = Some (put_squel mmk "eq_rect");
+ congr = put_squel mmk "f_equal" ;
+ sym = put_squel mmk "sym_eq" }
let build_eq eq = get_squel eq.eq
let build_ind eq = get_squel eq.ind
@@ -217,12 +217,12 @@ let build_rect eq =
let eqT_pattern_mark = put_pat mmk "(eqT ?1 ?2 ?3)"
let eqT_pattern () = get_pat eqT_pattern_mark
-let eqT= { eq = put_squel mmk "eqT";
- ind = put_squel mmk "eqT_ind" ;
- rrec = None;
- rect = None;
- congr = put_squel mmk "congr_eqT" ;
- sym = put_squel mmk "sym_eqT" }
+let eqT = { eq = put_squel mmk "eqT";
+ ind = put_squel mmk "eqT_ind" ;
+ rrec = None;
+ rect = None;
+ congr = put_squel mmk "congr_eqT" ;
+ sym = put_squel mmk "sym_eqT" }
let idT_pattern_mark = put_pat mmk "(identityT ?1 ?2 ?3)"
let idT_pattern () = get_pat idT_pattern_mark
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 04:38:47 +0000