]> matita.cs.unibo.it Git - helm.git/commit
- grafiteSync no longer used
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 15 Oct 2010 12:17:16 +0000 (12:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 15 Oct 2010 12:17:16 +0000 (12:17 +0000)
commit99a43adccee356e3d6057f67114c5cf08518b3f3
tree044f670bd62ec29c6845648f23f6ea05d394efb6
parent560db5569f54fba5bded568699a33947f88df3ba
- grafiteSync no longer used
- grafiteTypes.status simplified
matita/components/grafite_engine/.depend
matita/components/grafite_engine/Makefile
matita/components/grafite_engine/grafiteSync.ml [deleted file]
matita/components/grafite_engine/grafiteSync.mli [deleted file]
matita/components/grafite_engine/grafiteTypes.ml
matita/components/grafite_engine/grafiteTypes.mli
matita/matita/matitaScript.ml
matita/matita/matitacLib.ml