]> matita.cs.unibo.it Git - helm.git/commit
Added new syntax Type[n] where n is a number.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 5 Dec 2008 23:12:39 +0000 (23:12 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 5 Dec 2008 23:12:39 +0000 (23:12 +0000)
commit266fe24a5a5548c30f597ccd38578877643404d3
treeec64acd7b21a1dc6dbe185d7fe6d9dbffb87c3b6
parentff52cc33b36594d156f8c7d4351ffe0a34730b62
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
helm/software/components/acic_content/cicNotationPt.ml
helm/software/components/acic_content/termAcicContent.ml
helm/software/components/cic_acic/cic2acic.ml
helm/software/components/cic_acic/cic2acic.mli
helm/software/components/cic_disambiguation/cicDisambiguate.ml
helm/software/components/content_pres/cicNotationParser.ml
helm/software/components/content_pres/content2pres.mli
helm/software/components/content_pres/sequent2pres.mli
helm/software/components/content_pres/termContentPres.ml
helm/software/components/ng_disambiguation/nCicDisambiguate.ml