]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ba7ab95) | patch
Patch to avoid double creation of metavariables changed to a simpler one
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 10 Dec 2010 10:58:22 +0000 (10:58 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 10 Dec 2010 10:58:22 +0000 (10:58 +0000)
commit9fff8ca8b7cd686b0f7b5e9df77349b7b67e1a58
tree75105bf38f860bf29b6e60a99560c971938bfb82tree | snapshot
parentba7ab956f87c7d483df0dc622f256c6c9d475c7dcommit | diff
Patch to avoid double creation of metavariables changed to a simpler one
that keeps disambiguating twice the term. The old patch introduced a few
bugs that were difficult to fix.
matita/components/ng_tactics/nTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.