]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 75f1cb2) | patch
guarded_by_constructor completely rewritten, fixed missing lift when generating the...
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 24 Apr 2008 13:01:26 +0000 (13:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 24 Apr 2008 13:01:26 +0000 (13:01 +0000)
commit7fa28badba2091f1e3d207f13743a1f68d6bf1f3
tree6ad8b83ee27f14ffa57c0b01f8177053b905ca5btree | snapshot
parent75f1cb233da81b8db172128c7e93493009c0754ecommit | diff
guarded_by_constructor completely rewritten, fixed missing lift when generating the context of an inductive type in guarded_by_destructors.
helm/software/components/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.