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

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

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Fri, 29 Jul 2005 08:10:41 +0000 (08:10 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Fri, 29 Jul 2005 08:10:41 +0000 (08:10 +0000)
commit	650e3b3c9ff0b9cafb76a0edf8139a53446937ba
tree	d86f25d37f6f31d9f92492808b47324dd5d75192	tree \| snapshot
parent	fafa203bb8521f516a0e87ef28d2cedccb72f795	commit \| diff

0. core_notation.ma splitted into coq.moo and core_notation.moo
1. 'include "coq.ma"' is now explicitly required to activate the notation of Coq
2. 'include "coq.ma"' added here and there in the tests
3. .ma headers updated

45 files changed:

helm/matita/buildTimeConf.ml.in		diff \| blob \| history
helm/matita/coq.moo	[new file with mode: 0644]	blob
helm/matita/core_notation.ma	[deleted file]	blob \| history
helm/matita/core_notation.moo	[new file with mode: 0644]	blob
helm/matita/matita.ml		diff \| blob \| history
helm/matita/matitaEngine.ml		diff \| blob \| history
helm/matita/matitaMathView.ml		diff \| blob \| history
helm/matita/matitaMisc.ml		diff \| blob \| history
helm/matita/matitadep.ml		diff \| blob \| history
helm/matita/tests/absurd.ma		diff \| blob \| history
helm/matita/tests/apply.ma		diff \| blob \| history
helm/matita/tests/assumption.ma		diff \| blob \| history
helm/matita/tests/auto.ma		diff \| blob \| history
helm/matita/tests/baseuri.ma		diff \| blob \| history
helm/matita/tests/change.ma		diff \| blob \| history
helm/matita/tests/clear.ma		diff \| blob \| history
helm/matita/tests/clearbody.ma		diff \| blob \| history
helm/matita/tests/coercions.ma		diff \| blob \| history
helm/matita/tests/comments.ma		diff \| blob \| history
helm/matita/tests/constructor.ma		diff \| blob \| history
helm/matita/tests/contradiction.ma		diff \| blob \| history
helm/matita/tests/cut.ma		diff \| blob \| history
helm/matita/tests/decompose.ma		diff \| blob \| history
helm/matita/tests/discriminate.ma		diff \| blob \| history
helm/matita/tests/elim.ma		diff \| blob \| history
helm/matita/tests/fguidi.ma		diff \| blob \| history
helm/matita/tests/first.ma		diff \| blob \| history
helm/matita/tests/fix_betareduction.ma		diff \| blob \| history
helm/matita/tests/fold.ma		diff \| blob \| history
helm/matita/tests/generalize.ma		diff \| blob \| history
helm/matita/tests/inversion.ma		diff \| blob \| history
helm/matita/tests/letrec.ma		diff \| blob \| history
helm/matita/tests/match_inference.ma		diff \| blob \| history
helm/matita/tests/mysql_escaping.ma		diff \| blob \| history
helm/matita/tests/paramodulation.ma		diff \| blob \| history
helm/matita/tests/record.ma		diff \| blob \| history
helm/matita/tests/replace.ma		diff \| blob \| history
helm/matita/tests/rewrite.ma		diff \| blob \| history
helm/matita/tests/second.ma		diff \| blob \| history
helm/matita/tests/simpl.ma		diff \| blob \| history
helm/matita/tests/test2.ma		diff \| blob \| history
helm/matita/tests/test3.ma		diff \| blob \| history
helm/matita/tests/test4.ma		diff \| blob \| history
helm/matita/tests/third.ma		diff \| blob \| history
helm/matita/tests/unfold.ma		diff \| blob \| history

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

RSS Atom