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

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

author	Enrico Tassi <enrico.tassi@inria.fr>
	Thu, 19 Jun 2008 11:18:58 +0000 (11:18 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Thu, 19 Jun 2008 11:18:58 +0000 (11:18 +0000)
commit	8c4659819a1c1f2e450d9a588ecca37d95ae48e9
tree	d0cb7006edb03ba81f6d2dfd0fa7818bc37349a8	tree \| snapshot
parent	275a432d33c455d75725d5991e82b62e7d01f68d	commit \| diff

notation on steroids: 'term 40 x' is a valid variable name in notation and
places 'x' at term level 40 even if the notation is placed elsewhere

18 files changed:

helm/software/components/acic_content/cicNotationEnv.ml		diff \| blob \| history
helm/software/components/acic_content/cicNotationEnv.mli		diff \| blob \| history
helm/software/components/acic_content/cicNotationPp.ml		diff \| blob \| history
helm/software/components/acic_content/cicNotationPt.ml		diff \| blob \| history
helm/software/components/content_pres/cicNotationParser.ml		diff \| blob \| history
helm/software/components/content_pres/cicNotationParser.mli		diff \| blob \| history
helm/software/components/content_pres/cicNotationPres.ml		diff \| blob \| history
helm/software/components/content_pres/termContentPres.ml		diff \| blob \| history
helm/software/components/content_pres/termContentPres.mli		diff \| blob \| history
helm/software/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
helm/software/components/lexicon/cicNotation.ml		diff \| blob \| history
helm/software/matita/core_notation.moo		diff \| blob \| history
helm/software/matita/library/algebra/finite_groups.ma		diff \| blob \| history
helm/software/matita/library/algebra/groups.ma		diff \| blob \| history
helm/software/matita/library/demo/power_derivative.ma		diff \| blob \| history
helm/software/matita/library/demo/realisability.ma		diff \| blob \| history
helm/software/matita/library/list/list.ma		diff \| blob \| history
helm/software/matita/library/nat/permutation.ma		diff \| blob \| history

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