]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 095eaa9) | patch
- removed MQueryMisc. Ratio: it was used only for transformation uri -> term.
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 22 Oct 2004 12:38:30 +0000 (12:38 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 22 Oct 2004 12:38:30 +0000 (12:38 +0000)
commitfafcc706c1ecd6a3966a9b9de72c0de9f494dabe
treec4faceb178c24bcd07db9a0b2d7f1dfeff7fc937tree | snapshot
parent095eaa933206f18b77cadd92260c6aea821d08cdcommit | diff
- removed MQueryMisc. Ratio: it was used only for transformation uri -> term.
  The same feature is now available directly in CicUtil without the need
  of cic_textual_parser URIs
helm/ocaml/mathql/.depend diff | blob | history
helm/ocaml/mathql/Makefile diff | blob | history
helm/ocaml/mathql/mQueryMisc.ml [deleted file] blob | history
helm/ocaml/mathql/mQueryMisc.mli [deleted file] blob | history
Unnamed repository; edit this file 'description' to name the repository.