]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 56117fb) | patch
1. added a test for injection
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 14 Sep 2006 11:58:21 +0000 (11:58 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 14 Sep 2006 11:58:21 +0000 (11:58 +0000)
commit56fabdc3616fef02243e64eda35a81df606d0586
tree5e1afbe11718826658399c8fc73f6cff13b0d9b6tree | snapshot
parent56117fb4613ccd685861ca762954169c059467c8commit | diff
1. added a test for injection
2. injection now works also on inductive types with left parameters

As the test shows, there are still bugs even in the case of an inductive
case with right parameters only.
components/tactics/discriminationTactics.ml diff | blob | history
matita/tests/injection.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.