]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5ae174c) | patch
(Approximated) inference of relevance implemented: an argument X of t is irrelevant
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 15 May 2008 17:04:07 +0000 (17:04 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 15 May 2008 17:04:07 +0000 (17:04 +0000)
commite8a373c61ed58f91682b16c753d1926fa647fa7d
treee9852c3b05ea35dfe58ab73011d06fdc5cc9ac67tree | snapshot
parent5ae174c1243ae83ceeda6f2641d12565842d250fcommit | diff
(Approximated) inference of relevance implemented: an argument X of t is irrelevant
if it has sort Prop and the sort of t is not Prop.
helm/software/components/ng_kernel/oCic2NCic.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.