]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0f8a03b) | patch
Great optimization for eat_prods: if the type of the head of the application is meta_...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 26 May 2006 11:18:47 +0000 (11:18 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 26 May 2006 11:18:47 +0000 (11:18 +0000)
commitbba18e224460b5140bf50ef5750e3993e4a32a01
treeca04ff6201302b26148d34a21236f756e8700c4btree | snapshot
parent0f8a03b999acc2a16cbbffd6b19ab0e2967587cccommit | diff
Great optimization for eat_prods: if the type of the head of the application is meta_closed,
the construction of the spine of Prods and relative unification is skipped.
components/cic_unification/cicRefine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.