]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9e0de99) | patch
new implementation (due to paths).
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 24 Jun 2005 17:22:56 +0000 (17:22 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 24 Jun 2005 17:22:56 +0000 (17:22 +0000)
commitcaaca5ed51e45a023ccb1244fd5cbbb32d233e2e
tree92af409f8016d3fd8d0c730e3ad4cf265d2c02fetree | snapshot
parent9e0de9924a24c8b34b3738ba343334f761c3471dcommit | diff
new implementation (due to paths).
terms found by select (that may be under some binders) are delifted to the
context and, once reduced, lifted back.
helm/ocaml/tactics/reductionTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.