]> matita.cs.unibo.it Git - helm.git/commit
do not apply hints if metaclosed
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 22 Jul 2010 08:03:45 +0000 (08:03 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 22 Jul 2010 08:03:45 +0000 (08:03 +0000)
commite1625ad8b8065269c7d7395a8675780228259657
tree216181517e261479aff490f559cf0e5d3329f8eb
parentf57cdba1f7cad1891a2fcc38432f73a584d47e48
do not apply hints if metaclosed
helm/software/components/ng_refiner/nCicUnification.ml