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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 19 Jun 2015 16:58:43 +0000 (16:58 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 19 Jun 2015 16:58:43 +0000 (16:58 +0000)
commit	67686e04702688cc822e809e5168f765bf69d7cb
tree	4a97a50ccbd52cc2071914e974fc92d14afbd0d8	tree \| snapshot
parent	1be981691870cca039b1af1fb954491c2020d483	commit \| diff

new options activated
- tracing can be restricted to specific constants with -b and -e
- restricted applications are now used by default for Automath inputs
use -n to activate extended applications
(this may lead to longer computations)

28 files changed:

helm/software/helena/Makefile		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_ag/bagOutput.ml		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/brg.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgCrg.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgELPI.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgELPI.mli		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/brgOutput.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgReduction.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgSubstitution.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgType.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgUntrusted.ml		diff \| blob \| history
helm/software/helena/src/basic_rg/brgValidity.ml		diff \| blob \| history
helm/software/helena/src/common/layer.ml		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/complete_rg/crgOutput.ml		diff \| blob \| history
helm/software/helena/src/text/txtCrg.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/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