]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1dbbb98) | patch
Bug fixed: a ~with_cast is now inserted when appropriate to avoid translation
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 4 Jul 2007 20:19:24 +0000 (20:19 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 4 Jul 2007 20:19:24 +0000 (20:19 +0000)
commit5b4ac2b6e69b6929c5fd81d8f3206adb9b974efc
treee9c72c31dd5aa3799b08fd706330d3440d40e7f0tree | snapshot
parent1dbbb98181ab7c40ed2da6a941a69833b00a6aaecommit | diff
Bug fixed: a ~with_cast is now inserted when appropriate to avoid translation
of a bottom-up conversion into a top-down conversion.
components/tactics/declarative.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.