]> matita.cs.unibo.it Git - helm.git/commit
hgdome no longer used (RIP)
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 8 Oct 2010 11:18:01 +0000 (11:18 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 8 Oct 2010 11:18:01 +0000 (11:18 +0000)
commite2dde4cca0fe3ce74a79edbf8cb7a0f8e616daa9
tree3c01ecd8a6dafc7a2cf7dc50922f91499b18ce39
parent46391de034097f7d10f2d3ab937bfb4726cb8e8b
hgdome no longer used (RIP)
15 files changed:
matita/components/METAS/meta.helm-hgdome.src [deleted file]
matita/components/Makefile
matita/components/hgdome/.depend [deleted file]
matita/components/hgdome/.depend.opt [deleted file]
matita/components/hgdome/Makefile [deleted file]
matita/components/hgdome/domMisc.ml [deleted file]
matita/components/hgdome/domMisc.mli [deleted file]
matita/components/hgdome/xml2Gdome.ml [deleted file]
matita/components/hgdome/xml2Gdome.mli [deleted file]
matita/configure.ac
matita/matita/applyTransformation.ml
matita/matita/applyTransformation.mli
matita/matita/matitaEngine.ml
matita/matita/matitaGuiTypes.mli
matita/matita/matitaMathView.ml