matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Enrico Tassi <enrico.tassi@inria.fr>
	Tue, 16 May 2006 08:29:31 +0000 (08:29 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Tue, 16 May 2006 08:29:31 +0000 (08:29 +0000)
commit	58955ec841575330f0b429033264f9ec7df319f9
tree	cc88e7906f3a09e6be591dd64b237fe36497b9c6	tree \| snapshot
parent	54d0b2c2a2956c76cc3109760552bbd26772ce3f	commit \| diff

utf8_macros moved to syntax_extensions.
quoting for inline profiling added

35 files changed:

helm/software/components/METAS/meta.helm-content_pres.src		diff \| blob \| history
helm/software/components/METAS/meta.helm-syntax_extensions.src	[new file with mode: 0644]	blob
helm/software/components/METAS/meta.helm-utf8_macros.src	[deleted file]	blob \| history
helm/software/components/Makefile		diff \| blob \| history
helm/software/components/acic_content/cicNotationPp.ml		diff \| blob \| history
helm/software/components/binaries/saturate/Makefile		diff \| blob \| history
helm/software/components/content_pres/Makefile		diff \| blob \| history
helm/software/components/grafite_parser/Makefile		diff \| blob \| history
helm/software/components/syntax_extensions/.depend	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/Makefile	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/README.syntax	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/data/dictionary-tex.xml	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/data/entities-table.xml	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/data/extra-entities.xml	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/make_table.ml	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/pa_unicode_macro.ml	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/profiling_macros.ml	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/test.ml	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/utf8Macro.ml	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/utf8Macro.mli	[new file with mode: 0644]	blob
helm/software/components/syntax_extensions/utf8MacroTable.ml	[new file with mode: 0644]	blob
helm/software/components/tactics/.depend		diff \| blob \| history
helm/software/components/tactics/Makefile		diff \| blob \| history
helm/software/components/utf8_macros/.depend	[deleted file]	blob \| history
helm/software/components/utf8_macros/Makefile	[deleted file]	blob \| history
helm/software/components/utf8_macros/README.syntax	[deleted file]	blob \| history
helm/software/components/utf8_macros/data/dictionary-tex.xml	[deleted file]	blob \| history
helm/software/components/utf8_macros/data/entities-table.xml	[deleted file]	blob \| history
helm/software/components/utf8_macros/data/extra-entities.xml	[deleted file]	blob \| history
helm/software/components/utf8_macros/make_table.ml	[deleted file]	blob \| history
helm/software/components/utf8_macros/pa_unicode_macro.ml	[deleted file]	blob \| history
helm/software/components/utf8_macros/test.ml	[deleted file]	blob \| history
helm/software/components/utf8_macros/utf8Macro.ml	[deleted file]	blob \| history
helm/software/components/utf8_macros/utf8Macro.mli	[deleted file]	blob \| history
helm/software/components/utf8_macros/utf8MacroTable.ml	[deleted file]	blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom