]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1561ac9) | patch
New reduction strategy (that behaves much better during simplification).
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Jan 2006 18:52:13 +0000 (18:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Jan 2006 18:52:13 +0000 (18:52 +0000)
commitef3f78973c2fa3151c09681bcdb60107cd73c518
treecd5c76b1572700882a3d3e815a9c04af581d3938tree | snapshot
parent1561ac998b6823c9e763617fcb9cf3c063bb5e3bcommit | diff
New reduction strategy (that behaves much better during simplification).
Unfortunately, the new reduction is a bit slower on one test (paramodulation).
To be investigated.
helm/matita/library/algebra/groups.ma diff | blob | history
helm/matita/library/nat/lt_arith.ma diff | blob | history
helm/ocaml/cic_proof_checking/cicReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.