]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0be569e) | patch
a bit of sharing and the optimization of not folding trough the metasenv if the to_be...
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 7 May 2007 11:38:56 +0000 (11:38 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 7 May 2007 11:38:56 +0000 (11:38 +0000)
commit49b788e968f88f6dcf20590d8bdb0788be87c4a4
treeaaca5fc064df5d7489b274616989e2d96540a2eftree | snapshot
parent0be569e573dcad311bcd55212fd3fcf2c37be0ffcommit | diff
a bit of sharing and the optimization of not folding trough the metasenv if the to_be_restrincted list is empty
helm/software/components/cic_unification/cicMetaSubst.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.