]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 732a2fb) | patch
Match in classification of non-terms taken in account.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 28 Aug 2012 16:11:37 +0000 (16:11 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 28 Aug 2012 16:11:37 +0000 (16:11 +0000)
commitd737336c89a9942ebe97a834ff87861c8907d6ab
tree84995125c9419573d22cefebc6f135064883b05etree | snapshot
parent732a2fb72cb93c13d5e6371386f7159325a9da19commit | diff
Match in classification of non-terms taken in account.
We take the sup of the classification of all branches according to the
order

`Proposition < `PropKind < `Type < `Kind < `KindOrType
matita/components/ng_kernel/nCicExtraction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.