]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8049c16) | patch
The left parameters coming from the constructor types have been refined in a
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 16 Sep 2009 08:32:32 +0000 (08:32 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 16 Sep 2009 08:32:32 +0000 (08:32 +0000)
commitd6ba7f4b8fbd98f2f1c848857022ef5fba80db53
treec79fdb91210a34a467f9d4c09a1fc0879ed748d2tree | snapshot
parent8049c166a37789d7a1b1ca1c3a1174712bbf87bacommit | diff
The left parameters coming from the constructor types have been refined in a
longer context. Thus we need to unify them in the longer context (that does not
hurt those coming from the inductive types).
helm/software/components/ng_refiner/nCicRefiner.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.