]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8a660ee) | patch
- hmysql removed (RIP)
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 8 Oct 2010 10:30:47 +0000 (10:30 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 8 Oct 2010 10:30:47 +0000 (10:30 +0000)
commitb8dac1f8f6b664b78e58c152cd3960e121713f5d
tree499edacf7b41217d80230269a1c3ff78fed17fe3tree | snapshot
parent8a660ee06d72cfee52c707bb1d8d8be3bab0d682commit | diff
- hmysql removed (RIP)
- library simplified to handle only new files, moo and lexicon
- BROKEN FEATURES: recursive decompilation of library files is currently
  broken since, without the db, there is currently no way to compute the
  reverse dependencies
49 files changed:
matita/components/METAS/meta.helm-hmysql.src [deleted file] blob | history
matita/components/METAS/meta.helm-library.src diff | blob | history
matita/components/METAS/meta.helm-ng_kernel.src diff | blob | history
matita/components/Makefile diff | blob | history
matita/components/binaries/Makefile diff | blob | history
matita/components/binaries/heights/.depend [deleted file] blob | history
matita/components/binaries/heights/.depend.opt [deleted file] blob | history
matita/components/binaries/heights/Makefile [deleted file] blob | history
matita/components/binaries/heights/heights.conf.xml [deleted file] blob | history
matita/components/binaries/heights/heights.ml [deleted file] blob | history
matita/components/binaries/transcript/grafite.ml diff | blob | history
matita/components/grafite_engine/grafiteEngine.ml diff | blob | history
matita/components/grafite_engine/grafiteSync.ml diff | blob | history
matita/components/grafite_engine/grafiteSync.mli diff | blob | history
matita/components/grafite_engine/grafiteTypes.ml diff | blob | history
matita/components/grafite_engine/grafiteTypes.mli diff | blob | history
matita/components/hmysql/.depend [deleted file] blob | history
matita/components/hmysql/.depend.opt [deleted file] blob | history
matita/components/hmysql/Makefile [deleted file] blob | history
matita/components/hmysql/hMysql.ml [deleted file] blob | history
matita/components/hmysql/hSql.ml [deleted file] blob | history
matita/components/hmysql/hSql.mli [deleted file] blob | history
matita/components/hmysql/hSqlite3.ml [deleted file] blob | history
matita/components/library/.depend [deleted file] blob | history
matita/components/library/.depend.opt [deleted file] blob | history
matita/components/library/Makefile [deleted file] blob | history
matita/components/library/cicCoercion.ml [deleted file] blob | history
matita/components/library/cicCoercion.mli [deleted file] blob | history
matita/components/library/cicFix.ml [deleted file] blob | history
matita/components/library/cicFix.mli [deleted file] blob | history
matita/components/library/coercDb.ml [deleted file] blob | history
matita/components/library/coercDb.mli [deleted file] blob | history
matita/components/library/librarian.ml [deleted file] blob | history
matita/components/library/librarian.mli [deleted file] blob | history
matita/components/library/libraryClean.ml [deleted file] blob | history
matita/components/library/libraryClean.mli [deleted file] blob | history
matita/components/library/libraryDb.ml [deleted file] blob | history
matita/components/library/libraryDb.mli [deleted file] blob | history
matita/components/library/libraryMisc.ml [deleted file] blob | history
matita/components/library/libraryMisc.mli [deleted file] blob | history
matita/components/library/librarySync.ml [deleted file] blob | history
matita/components/library/librarySync.mli [deleted file] blob | history
matita/components/ng_refiner/nCicCoercion.ml diff | blob | history
matita/components/ng_refiner/nCicCoercion.mli diff | blob | history
matita/matita/matitaExcPp.ml diff | blob | history
matita/matita/matitaInit.ml diff | blob | history
matita/matita/matitaScript.ml diff | blob | history
matita/matita/matitacLib.ml diff | blob | history
matita/matita/matitaclean.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.