]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a164faf) | 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)
commitf6263eadaa2b8d0bc0c2a5a944e0d4641c356fe9
tree1c764cfd4af1b7532d251bf4f4ae5f5ab0227833tree | snapshot
parenta164faf27d1f9b910a39b19025f110f4738bead7commit | 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.
components/tactics/discriminationTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.