]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7bbe9c8) | 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)
commit3a0c3a4275ba88babc9d5717a019fe277d947fa6
treef9c71816c6d949cc99c9d5b51a85e9564c86b691tree | snapshot
parent7bbe9c8a9fcc471920c18a12fb5745828f2fd188commit | 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.
helm/software/components/tactics/discriminationTactics.ml diff | blob | history
helm/software/matita/tests/injection.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.