]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 21d5872) | patch
added begin list and end list comments to help moogle search engine plugin
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 10 Jan 2005 10:47:47 +0000 (10:47 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 10 Jan 2005 10:47:47 +0000 (10:47 +0000)
commit3f6f868f14eadef7f17d5e3008cffe19307ad492
tree64b9e6f97fbd30a1c68f0d767f2e6c528339c76etree | snapshot
parent21d58727027699d8617a7faab912843756b585edcommit | diff
added begin list and end list comments to help moogle search engine plugin
helm/searchEngine/mooglePp.ml diff | blob | history
helm/searchEngine/searchEngine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.