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

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

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Tue, 28 Jul 2009 15:17:51 +0000 (15:17 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Tue, 28 Jul 2009 15:17:51 +0000 (15:17 +0000)
commit	d34061fd1c820139fad38c39dee6377e5057bf26
tree	0dc6b7a43ed77e927e984df4f3238f438d2a9dd9	tree \| snapshot
parent	ee7855524284ea3a282c68f22ffa36e535a11810	commit \| diff

Introduction of vectors of implicit (only for NG).
Proposed concrete syntax: "..."

20 files changed:

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/cicNotationUtil.ml		diff \| blob \| history
helm/software/components/acic_content/termAcicContent.ml		diff \| blob \| history
helm/software/components/cic/cicUtil.ml		diff \| blob \| history
helm/software/components/cic_disambiguation/cicDisambiguate.ml		diff \| blob \| history
helm/software/components/content_pres/cicNotationLexer.ml		diff \| blob \| history
helm/software/components/content_pres/cicNotationParser.ml		diff \| blob \| history
helm/software/components/content_pres/content2presMatcher.ml		diff \| blob \| history
helm/software/components/content_pres/termContentPres.ml		diff \| blob \| history
helm/software/components/disambiguation/disambiguate.ml		diff \| blob \| history
helm/software/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
helm/software/components/ng_cic_content/nTermCicContent.ml		diff \| blob \| history
helm/software/components/ng_disambiguation/nCicDisambiguate.ml		diff \| blob \| history
helm/software/components/ng_kernel/nCic.ml		diff \| blob \| history
helm/software/components/ng_kernel/nCicPp.ml		diff \| blob \| history
helm/software/components/ng_tactics/nCicElim.ml		diff \| blob \| history
helm/software/components/ng_tactics/nTactics.ml		diff \| blob \| history
helm/software/components/tptp_grafite/tptp2grafite.ml		diff \| blob \| history
helm/software/matita/matitaScript.ml		diff \| blob \| history

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