]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8cbaf41) | patch
Almost always correct optimization: during unification, a meta-closed term and
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 12 Mar 2008 18:52:54 +0000 (18:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 12 Mar 2008 18:52:54 +0000 (18:52 +0000)
commitf45e7c2b52e83e4461056d386dcb768d7b25df05
tree792c351ff001c56befa45691f7089803dad9308btree | snapshot
parent8cbaf41588bb862705690b37aa856b6505611274commit | diff
Almost always correct optimization: during unification, a meta-closed term and
a term that is not meta closed are not tried for convertibility. This greatly
speeds up, for instance, some examples in Bertrand.
helm/software/components/cic_unification/cicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.