]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 14c956f) | patch
rewrite tactic: bug fix in rewriting under Pi's:
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 10 Mar 2007 22:23:38 +0000 (22:23 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 10 Mar 2007 22:23:38 +0000 (22:23 +0000)
commit5813d9a88f34f0c0d15cb74243f638d02ae163fa
treedcc2857efac56f8757d42c3e4bc1973339cd883atree | snapshot
parent14c956f9be9e525fc2dd140e8a2ea6c063c48930commit | diff
rewrite tactic: bug fix in rewriting under Pi's:
                the application context of the subterm to rewrite can not be
forgotten
components/tactics/equalityTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.