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

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

projects / helm.git / commit

summary | shortlog | log | commit | commitdiff | tree
(parent: ff52cc3) | patch

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Fri, 5 Dec 2008 23:12:39 +0000 (23:12 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Fri, 5 Dec 2008 23:12:39 +0000 (23:12 +0000)
commit	266fe24a5a5548c30f597ccd38578877643404d3
tree	ec64acd7b21a1dc6dbe185d7fe6d9dbffb87c3b6	tree \| snapshot
parent	ff52cc33b36594d156f8c7d4351ffe0a34730b62	commit \| diff

Added new syntax Type[n] where n is a number.
The old kernel interpretes it simply as Type.
The new kernel as Typen.

helm/software/components/acic_content/cicNotationPp.ml		diff \| blob \| history
helm/software/components/acic_content/cicNotationPt.ml		diff \| blob \| history
helm/software/components/acic_content/termAcicContent.ml		diff \| blob \| history
helm/software/components/cic_acic/cic2acic.ml		diff \| blob \| history
helm/software/components/cic_acic/cic2acic.mli		diff \| blob \| history
helm/software/components/cic_disambiguation/cicDisambiguate.ml		diff \| blob \| history
helm/software/components/content_pres/cicNotationParser.ml		diff \| blob \| history
helm/software/components/content_pres/content2pres.mli		diff \| blob \| history
helm/software/components/content_pres/sequent2pres.mli		diff \| blob \| history
helm/software/components/content_pres/termContentPres.ml		diff \| blob \| history
helm/software/components/ng_disambiguation/nCicDisambiguate.ml		diff \| blob \| history

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