]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e09745b) | 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)
commitb934a94a5d005f9d8e668ef49ec83487090a787b
tree5b3f950675715b69b26c2034450b8f1448139b48tree | snapshot
parente09745b16df1d7a897cddfb6a79b8f8572de1380commit | 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.
components/cic_unification/cicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.