]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f969eae) | patch
Patch to the unification to make the case (i l) vs (t l) work when i is
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 26 Jul 2006 15:50:54 +0000 (15:50 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 26 Jul 2006 15:50:54 +0000 (15:50 +0000)
commitacfce0988db6cce820044b174f4f485dc0a0c6ec
tree121895b6435ea89322479cda006357d7f8ce4691tree | snapshot
parentf969eaeae57e6d4b1c7e9b35d4061134094d5266commit | diff
Patch to the unification to make the case (i l) vs (t l) work when i is
an inductive type and (t l) must be subject to weak head reduction.
helm/software/components/cic_unification/cicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.