]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c19ffb6) | patch
New implementation of eat_prods.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 26 Feb 2004 16:14:58 +0000 (16:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 26 Feb 2004 16:14:58 +0000 (16:14 +0000)
commitda11c92be86c24285ef1a4d0ddfe1e074a6b322a
tree2ad57f4f535815c791490fb1223dac943a8fbe88tree | snapshot
parentc19ffb699f8f4681f0c7d9f59fae96f2023cd058commit | diff
New implementation of eat_prods.
In theory we expected it to be less efficient.
In pratice it is MUCH more efficient.

The old implementation is still there, but commented out.
We have to investigate the mistery a bit more.
helm/ocaml/cic_unification/cicRefine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.