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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 11 Nov 2014 12:23:46 +0000 (12:23 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 11 Nov 2014 12:23:46 +0000 (12:23 +0000)
commit	aaafdf833247fc188049ab519d734d92f7e03333
tree	fdb98398112035eda5ccb947b0df2370967fe8e8	tree \| snapshot
parent	a46a0dcfd97373045074ad421df89a66e3199628	commit \| diff

- commit completed :)
typechecking is approx. fast as before,
validation is slightly faster than typechecking.
for now the new RTM is slightly slower than the old one
- we commit three versions of the grundlagen:
0 (original)
1 (no eta-conversion)
2 (no eta-conversion, no @-typing)

helm/software/helena/Makefile		diff \| blob \| history
helm/software/helena/examples/grundlagen/grundlagen.aut	[deleted file]	blob \| history
helm/software/helena/examples/grundlagen/grundlagen_0.aut	[new file with mode: 0644]	blob
helm/software/helena/examples/grundlagen/grundlagen_1.aut	[new file with mode: 0644]	blob
helm/software/helena/examples/grundlagen/grundlagen_2.aut	[new file with mode: 0644]	blob
helm/software/helena/src/basic_rg/brgReduction.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgType.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgValidity.ml		diff \| blob \| history
helm/software/helena/src/common/status.ml		diff \| blob \| history

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

RSS Atom