]> matita.cs.unibo.it Git - helm.git/commit
New version: only new nodes are normalized; moreover, reduction stops as soon
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Mar 2009 11:47:13 +0000 (11:47 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Mar 2009 11:47:13 +0000 (11:47 +0000)
commitdd70926289053cdc003776a5074d2262a2ec8243
tree918969905487e9ea0d4a5157f79f21c158bec4af
parent7bc72d8afaebb1d2070a26b07f9bf4242b648e2c
New version: only new nodes are normalized; moreover, reduction stops as soon
as the term becomes shorter.
helm/software/matita/contribs/formal_topology/bin/Makefile
helm/software/matita/contribs/formal_topology/bin/comb.ml