]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 708e70e) | patch
Universe.key was not used to index terms, but was used to retrieve them
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 26 May 2008 13:58:13 +0000 (13:58 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 26 May 2008 13:58:13 +0000 (13:58 +0000)
commitd0e058e37a75dcb0247b0b0efbe99e68ce1ceca4
treec5ac89166d6923ad1b437fc21df75abbf5bd27a9tree | snapshot
parent708e70e2b90c71c9caedef2665a8d4971cf7b8d9commit | diff
Universe.key was not used to index terms, but was used to retrieve them
helm/software/components/tactics/autoCache.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.