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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 5 Jun 2009 22:18:01 +0000 (22:18 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 5 Jun 2009 22:18:01 +0000 (22:18 +0000)
commit	8ae1653eb75d2b57c50e077c49cb9d078313ea9d
tree	24f9a42870467b09afc06e042a9312966c19203d	tree \| snapshot
parent	b97a7976503b2d2e5cbc9199f848135a324775a8	commit \| diff

- Procedural convertible rewrites in the conclusion are now detected and replaced by change
- grafiteAst: semantics of the Include flag changed: now true means normal include, New Inline flags Coercions, Comments (activated) Debug (not yet)
- library: eq_plus_Zplus moved from Z/times to Z/plus

now Z/plus.ma Z/times.ma are fully reconstructed :)

24 files changed:

helm/software/components/acic_procedural/acic2Procedural.ml		diff \| blob \| history
helm/software/components/acic_procedural/procedural2.ml		diff \| blob \| history
helm/software/components/acic_procedural/proceduralConversion.ml		diff \| blob \| history
helm/software/components/acic_procedural/proceduralConversion.mli		diff \| blob \| history
helm/software/components/acic_procedural/proceduralHelpers.ml		diff \| blob \| history
helm/software/components/acic_procedural/proceduralHelpers.mli		diff \| blob \| history
helm/software/components/acic_procedural/proceduralOptimizer.ml		diff \| blob \| history
helm/software/components/binaries/transcript/.depend.opt		diff \| blob \| history
helm/software/components/binaries/transcript/engine.ml		diff \| blob \| history
helm/software/components/binaries/transcript/gallina8Parser.mly		diff \| blob \| history
helm/software/components/binaries/transcript/grafite.ml		diff \| blob \| history
helm/software/components/grafite/grafiteAst.ml		diff \| blob \| history
helm/software/components/grafite/grafiteAstPp.ml		diff \| blob \| history
helm/software/components/grafite_parser/dependenciesParser.ml		diff \| blob \| history
helm/software/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
helm/software/components/ng_paramodulation/.depend		diff \| blob \| history
helm/software/components/ng_paramodulation/.depend.opt		diff \| blob \| history
helm/software/components/tptp_grafite/tptp2grafite.ml		diff \| blob \| history
helm/software/matita/applyTransformation.ml		diff \| blob \| history
helm/software/matita/contribs/procedural/library/library.conf.xml		diff \| blob \| history
helm/software/matita/library/Z/plus.ma		diff \| blob \| history
helm/software/matita/library/Z/times.ma		diff \| blob \| history
helm/software/matita/matita.lang		diff \| blob \| history
helm/software/matita/matitacLib.ml		diff \| blob \| history

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

RSS Atom