]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0d681e0) | patch
This commit makes ProofEngineHelpers.select reach its full potentials.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Jun 2005 08:44:39 +0000 (08:44 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Jun 2005 08:44:39 +0000 (08:44 +0000)
commitfa2c122dc2d20e0d8b473bef9128464c3477d419
treeabbce415933f035cc1a984d38c40185bb34d1fdctree | snapshot
parent0d681e06c6ced0be7f9dbce417684b082229745acommit | diff
This commit makes ProofEngineHelpers.select reach its full potentials.
Its arguments are now a conjecture and a pattern and its output is
a conjecture-like structure made of physical pointers to matching subterms
(together with their contexts).
helm/ocaml/tactics/proofEngineHelpers.ml diff | blob | history
helm/ocaml/tactics/proofEngineHelpers.mli diff | blob | history
helm/ocaml/tactics/reductionTactics.ml diff | blob | history
helm/ocaml/tactics/variousTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.