]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6a1f139) | patch
Bug fixed in simplify: delta expansion of constants applied to more arguments
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 22 Feb 2006 21:17:16 +0000 (21:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 22 Feb 2006 21:17:16 +0000 (21:17 +0000)
commite1b382b7a82e69cb009571017c16a3665f9946c4
treeb6aeb07e27392d535cdf4c54270eda8541cb71d7tree | snapshot
parent6a1f139f8255ee861d8a30779555d72a708478eccommit | diff
Bug fixed in simplify: delta expansion of constants applied to more arguments
than head lambda abstractions was always performed (even if no "interesting"
reduction took place).
helm/software/components/tactics/proofEngineReduction.ml diff | blob | history
helm/software/matita/library/algebra/groups.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.