]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 61cae68) | 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)
commit0f06e39d49460377dfa214b3d471b71cb9111f48
tree7db170a06da611bc3161934c6247d4806e7c1e73tree | snapshot
parent61cae682fe37db1a53a186ae5e10cfae47a89396commit | 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).
components/tactics/proofEngineReduction.ml diff | blob | history
matita/library/algebra/groups.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.