]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2cfd3d2) | patch
aded some whd, you should be able to declare something like:
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Dec 2008 13:12:28 +0000 (13:12 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Dec 2008 13:12:28 +0000 (13:12 +0000)
commit82f61808091c59aa884eb232b96ee1c655dcb39a
tree5fc73893760886b7edbf13eef0f9f4bfde8f0c08tree | snapshot
parent2cfd3d24d73634238d5eaf40f91e12c10fe28d71commit | diff
aded some whd, you should be able to declare something like:
 inductive A : FOO :=
where FOO is defined as a sort (or unfolds to somthing ending with a sort)
helm/software/components/library/cicElim.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.