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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 25 Nov 2008 19:27:41 +0000 (19:27 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 25 Nov 2008 19:27:41 +0000 (19:27 +0000)
commit	0b76904a3f10bfd6390d26172fd6979626bd72f4
tree	2165a70affe86c8d1b8dd863cd177cfc781987cf	tree \| snapshot
parent	d62f34ee8014169ba1e44669ab815b006780f454	commit \| diff

cicUtil: we moved here pp_term from proceduralHelpers
cicDischarge: some bugs fixed
transcript: we now support explicit declaration of dependences
procedural/Coq: we added an explicit dependence to Init/Prelude where needed

32 files changed:

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/engine.ml		diff \| blob \| history
helm/software/components/cic/cicUtil.ml		diff \| blob \| history
helm/software/components/cic/cicUtil.mli		diff \| blob \| history
helm/software/components/cic_proof_checking/cicDischarge.ml		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/EqNat.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Even.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Le.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Bool/Bool.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Bool/DecBool.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Bool/Sumbool.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Coq.conf.xml		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Lists/Streams.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Berardi.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/ChoiceFacts.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/ClassicalFacts.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Decidable.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Eqdep.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Eqdep_dec.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Hurkens.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/RelationalChoice.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/NArith/BinPos.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Relations/Relation_Definitions.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Relations/Rstar.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Setoids/Setoid.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Ensembles.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Permut.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Relations_1.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Wellfounded/Inverse_Image.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/depends		diff \| blob \| history

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

RSS Atom