]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4421e8c) | patch
Automatic generation of elimination and inversion principles for co-inductive
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 31 Mar 2008 17:56:14 +0000 (17:56 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 31 Mar 2008 17:56:14 +0000 (17:56 +0000)
commit1633244fde7c007e23041b700da9d643596877e3
tree7faebd3a2eb80dc094365aff5d13ca60048a0cc1tree | snapshot
parent4421e8ce2ec9251e9e9e3a1a2c2ab9405ddec77acommit | diff
Automatic generation of elimination and inversion principles for co-inductive
types disabled (since it does not make sense!)
helm/software/components/library/librarySync.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.