]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9c6a69b) | patch
Fixed a bug in the unification, which prevented some reduction steps from being
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Mon, 1 Mar 2010 18:07:54 +0000 (18:07 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Mon, 1 Mar 2010 18:07:54 +0000 (18:07 +0000)
commit511421f12dd04547bbf1206470e5d39237673429
treef9fbbde90eaf13683db68d8305de6cd3137a7ce9tree | snapshot
parent9c6a69b957895d429f1c8d3ae4cebe529ab70433commit | diff
Fixed a bug in the unification, which prevented some reduction steps from being
performed in the case "match vs. match", when the types of the matching term
were not the same. The procedure used to always raise an Uncertain exception,
while in many cases the good choice would be to raise KeepReducing. This caused
the nnormalize tactic to fail with an error in some cases.
helm/software/components/ng_refiner/nCicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.