]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 63b1b04) | patch
Bug fixed:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 6 May 2010 15:15:46 +0000 (15:15 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 6 May 2010 15:15:46 +0000 (15:15 +0000)
commitc8767b56c0a77fa52efb3815524620602709922b
tree2c504b7a0eca179f01929cda897e679477fba266tree | snapshot
parent63b1b044e54bac3ffecc02ee2941b60f58b0c837commit | diff
Bug fixed:

 During unification of E1 with E2, E1 and E2 where not always reduced.
 In particular, reduction was not performed in the cases:
   LetIn vs LetIn, Match vs Match
 and maybe also in some cases Appl Meta vs Appl Meta (who knows?)
helm/software/components/ng_refiner/nCicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.