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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 27 Jun 2015 18:35:52 +0000 (18:35 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 27 Jun 2015 18:35:52 +0000 (18:35 +0000)
commit	2cf2e883f91164ce614bdc86b5c5e2419b98f68d
tree	af3d6ca2d923fb5005e38650c27d7770036294ac	tree \| snapshot
parent	98fef490e55d1d780e8c0bb19de0218e08ae73b1	commit \| diff

- bug fix in the static analyzer allows better Pi/forall separation (exportation to grafite)
- new option -y allows to use infinity-abstraction in contexts
- ages removed from global references (the RTM computes them)
- new semantics of the -g option (w.i.p.) for a comparison with Coq

23 files changed:

helm/software/helena/.depend.opt		diff \| blob \| history
helm/software/helena/Makefile		diff \| blob \| history
helm/software/helena/coq/grundlagen_2.v		diff \| blob \| history
helm/software/helena/matita/grundlagen_2.ma		diff \| blob \| history
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_rg/brg.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgEnvironment.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgGallina.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgGrafite.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgReduction.ml		diff \| blob \| history
helm/software/helena/src/common/entity.ml		diff \| blob \| history
helm/software/helena/src/common/layer.ml		diff \| blob \| history
helm/software/helena/src/common/layer.mli		diff \| blob \| history
helm/software/helena/src/common/options.ml		diff \| blob \| history
helm/software/helena/src/common/output.ml		diff \| blob \| history
helm/software/helena/src/complete_rg/crg.ml		diff \| blob \| history
helm/software/helena/src/text/txtCrg.ml		diff \| blob \| history
helm/software/helena/src/text/txtParser.mly		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/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