]> matita.cs.unibo.it Git - helm.git/commit
Passing the right subst and metasenv when indexing local equations.
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 21 Nov 2011 10:17:02 +0000 (10:17 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 21 Nov 2011 10:17:02 +0000 (10:17 +0000)
commit99d8a9f4c5d6e3b3052ec03189e02db6b817bc55
treea3cc598eae80ecb40e55402ecc62de6e6d2df3ad
parent4c2b24a41bec48da2f6b5abc0dda537f12578a87
Passing the right subst and metasenv when indexing local equations.
matita/components/ng_tactics/nnAuto.ml