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	4cdf45f08cd95641a094312ddc558320b874fa16
tree	d4abcc79e74fd5c392bd7c4f662a101b6778be37	tree \| snapshot
parent	5d8d504eb46d181d7a915b2be154022ea83da4df	commit \| diff

utf8_macros moved to syntax_extensions.
quoting for inline profiling added

35 files changed:

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

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

RSS Atom