]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1d973a0) | 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)
commit9151b08e0041e0e8d4823a92dbc12e120d6075f6
treed9db9b42718b2f500a8b23cec0cffd50c28bc1aetree | snapshot
parent1d973a067d441fbae43905abb704e21faa223e2bcommit | 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.
helm/software/components/cic_unification/cicRefine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.