]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0dc8115) | patch
New version (by Wilmer). The main difference w.r.t. previous one
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 11 Oct 2011 00:26:29 +0000 (00:26 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 11 Oct 2011 00:26:29 +0000 (00:26 +0000)
commit65d69375785f5e6ed48c944cdc3b4a526b5913e3
tree6f3c4d9e1b0983c77c2bacde589dc0cfa439ff51tree | snapshot
parent0dc8115859d7f482793315493adc0b619236e06ccommit | diff
New version (by Wilmer). The main difference w.r.t. previous one
is that it should not normalize the hypotheses and the conclusion
without any need to do that.

BEWARE: this version seems to be a little buggy. See "Wilmer: XXX"
comments in CerCo files. I commit it anyway and let the debug to
Wilmer. It only fails in three places.
matita/components/ng_tactics/nDestructTac.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.