]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 85521ef) | patch
* Fixed a couple of glitches in ndestruct
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 4 May 2010 16:49:59 +0000 (16:49 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 4 May 2010 16:49:59 +0000 (16:49 +0000)
commitab739c4972971725f59c52275a3257ebf524143f
treebef0d16d1c88951ee9cf006d54bfa3bef83433b7tree | snapshot
parent85521efd364ec494e4cc024bbf87182a312e1b7bcommit | diff
* Fixed a couple of glitches in ndestruct
  - blob equations were not always handled properly
  - tactic used to fail due to not optimal behaviour of the refiner
* Added (experimental) support for JM equality to ndestruct
helm/software/components/ng_tactics/nDestructTac.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.