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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 28 Nov 2014 15:23:48 +0000 (15:23 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 28 Nov 2014 15:23:48 +0000 (15:23 +0000)
commit	ac97468f5422efc770316286cb807e3d3245a474
tree	764a797e8d4afb788fec41e67012bc2a0fac8685	tree \| snapshot
parent	7562d9781dc4f351ddc3b2f8edd21f4976621948	commit \| diff

- the disambiguation of unified binders continues
- exportation to grafite is set up
- grundlagen_2: we disambiguate up to notion 6377, matita validates up
to notion 114

41 files changed:

helm/software/helena/.depend.opt		diff \| blob \| history
helm/software/helena/Makefile		diff \| blob \| history
helm/software/helena/examples/grundlagen/grundlagen_2.aut		diff \| blob \| history
helm/software/helena/grundlagen_2.ma	[new file with mode: 0644]	blob
helm/software/helena/root	[new file with mode: 0644]	blob
helm/software/helena/src/automath/autCrg.ml		diff \| blob \| history
helm/software/helena/src/basic_ag/bagCrg.ml		diff \| blob \| history
helm/software/helena/src/basic_ag/bagCrg.mli		diff \| blob \| history
helm/software/helena/src/basic_ag/bagOutput.ml		diff \| blob \| history
helm/software/helena/src/basic_ag/bagOutput.mli		diff \| blob \| history
helm/software/helena/src/basic_ag/bagReduction.ml		diff \| blob \| history
helm/software/helena/src/basic_ag/bagType.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/Make		diff \| blob \| history
helm/software/helena/src/basic_rg/brgGrafite.ml	[new file with mode: 0644]	blob
helm/software/helena/src/basic_rg/brgGrafite.mli	[new file with mode: 0644]	blob
helm/software/helena/src/basic_rg/brgOutput.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgOutput.mli		diff \| blob \| history
helm/software/helena/src/basic_rg/brgReduction.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgReduction.mli		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/Make		diff \| blob \| history
helm/software/helena/src/common/ccs.ml	[deleted file]	blob \| history
helm/software/helena/src/common/ccs.mli	[deleted file]	blob \| history
helm/software/helena/src/common/entity.ml		diff \| blob \| history
helm/software/helena/src/common/level.ml		diff \| blob \| history
helm/software/helena/src/common/level.mli		diff \| blob \| history
helm/software/helena/src/common/marks.ml		diff \| blob \| history
helm/software/helena/src/common/marks.mli		diff \| blob \| history
helm/software/helena/src/common/options.ml		diff \| blob \| history
helm/software/helena/src/complete_rg/crg.ml		diff \| blob \| history
helm/software/helena/src/complete_rg/crgOutput.ml		diff \| blob \| history
helm/software/helena/src/complete_rg/crgOutput.mli		diff \| blob \| history
helm/software/helena/src/lib/log.ml		diff \| blob \| history
helm/software/helena/src/lib/log.mli		diff \| blob \| history
helm/software/helena/src/modules.ml		diff \| blob \| history
helm/software/helena/src/toplevel/top.ml		diff \| blob \| history
helm/software/helena/src/xml/xmlCrg.ml		diff \| blob \| history
helm/software/helena/src/xml/xmlCrg.mli		diff \| blob \| history
helm/software/helena/src/xml/xmlLibrary.ml		diff \| blob \| history
helm/software/helena/src/xml/xmlLibrary.mli		diff \| blob \| history

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

RSS Atom