]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dd19b00) | patch
Bug fixed in injection: a missing lift bugged the tactic when the constructor
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 13 Sep 2006 12:53:01 +0000 (12:53 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 13 Sep 2006 12:53:01 +0000 (12:53 +0000)
commit82306753608353e9aed7e1b9c03b96787f1ec5eb
tree965475b30f55440e4c51e32178f7eb3106f80be0tree | snapshot
parentdd19b00878e9a29118141e8b178be6839c900ce9commit | diff
Bug fixed in injection: a missing lift bugged the tactic when the constructor
had more than one argument.
The tactic is still bugged when the inductive type has either right or left
parameters!
helm/software/components/tactics/discriminationTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.