]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5412a7f) | patch
Bug fixed in injection: injection can now work on inductive types that have
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 13 Sep 2006 17:22:21 +0000 (17:22 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 13 Sep 2006 17:22:21 +0000 (17:22 +0000)
commit6034f308db1dbe8d99d20a083e95b6b09c0a6613
tree70e15bc924847543c2a35ce8690c52f86e85fb8ctree | snapshot
parent5412a7f12ed2034b4dfb6104440a2308d6a6e8e1commit | diff
Bug fixed in injection: injection can now work on inductive types that have
right parameters. It is still bugged on inductive types with left parameters.
helm/software/components/tactics/discriminationTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.