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

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

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Tue, 11 Mar 2008 22:02:58 +0000 (22:02 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Tue, 11 Mar 2008 22:02:58 +0000 (22:02 +0000)
commit	cc23f034c9419186602d9250456241f2eba90d7c
tree	1ffb4c99bfa82aae644ac2eeaca69e84b42e724a	tree \| snapshot
parent	94538d45a28cf8e833f9ad4523b61a3252fde7d4	commit \| diff

Very experimental commit: the type of the source is now required in LetIns
and Defs. This is a back-porting from the new generation kernel.

TODO:
a) debug some failing examples (paramodulation)
b) port the code by Ferruccio
c) do something for Coq files (that are now rejected)

54 files changed:

helm/software/components/acic_content/acic2content.ml		diff \| blob \| history
helm/software/components/acic_content/cicNotationPp.ml		diff \| blob \| history
helm/software/components/acic_content/cicNotationUtil.ml		diff \| blob \| history
helm/software/components/acic_content/content.ml		diff \| blob \| history
helm/software/components/acic_content/content.mli		diff \| blob \| history
helm/software/components/acic_content/content2cic.ml		diff \| blob \| history
helm/software/components/acic_content/termAcicContent.ml		diff \| blob \| history
helm/software/components/acic_procedural/acic2Procedural.ml		diff \| blob \| history
helm/software/components/acic_procedural/proceduralConversion.ml		diff \| blob \| history
helm/software/components/acic_procedural/proceduralHelpers.ml		diff \| blob \| history
helm/software/components/acic_procedural/proceduralOptimizer.ml		diff \| blob \| history
helm/software/components/cic/cic.ml		diff \| blob \| history
helm/software/components/cic/cicInspect.ml		diff \| blob \| history
helm/software/components/cic/cicParser.ml		diff \| blob \| history
helm/software/components/cic/cicUtil.ml		diff \| blob \| history
helm/software/components/cic/deannotate.ml		diff \| blob \| history
helm/software/components/cic/unshare.ml		diff \| blob \| history
helm/software/components/cic_acic/cic2Xml.ml		diff \| blob \| history
helm/software/components/cic_acic/cic2acic.ml		diff \| blob \| history
helm/software/components/cic_acic/doubleTypeInference.ml		diff \| blob \| history
helm/software/components/cic_acic/eta_fixing.ml		diff \| blob \| history
helm/software/components/cic_disambiguation/disambiguate.ml		diff \| blob \| history
helm/software/components/cic_exportation/cicExportation.ml		diff \| blob \| history
helm/software/components/cic_proof_checking/cicMiniReduction.ml		diff \| blob \| history
helm/software/components/cic_proof_checking/cicPp.ml		diff \| blob \| history
helm/software/components/cic_proof_checking/cicReduction.ml		diff \| blob \| history
helm/software/components/cic_proof_checking/cicSubstitution.ml		diff \| blob \| history
helm/software/components/cic_proof_checking/cicTypeChecker.ml		diff \| blob \| history
helm/software/components/cic_proof_checking/cicUnivUtils.ml		diff \| blob \| history
helm/software/components/cic_proof_checking/freshNamesGenerator.ml		diff \| blob \| history
helm/software/components/cic_unification/cicMetaSubst.ml		diff \| blob \| history
helm/software/components/cic_unification/cicRefine.ml		diff \| blob \| history
helm/software/components/cic_unification/cicReplace.ml		diff \| blob \| history
helm/software/components/cic_unification/cicUnification.ml		diff \| blob \| history
helm/software/components/content_pres/termContentPres.ml		diff \| blob \| history
helm/software/components/metadata/metadataConstraints.ml		diff \| blob \| history
helm/software/components/metadata/metadataExtractor.ml		diff \| blob \| history
helm/software/components/tactics/auto.ml		diff \| blob \| history
helm/software/components/tactics/fourierR.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/equality.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/saturation.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/subst.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/utils.ml		diff \| blob \| history
helm/software/components/tactics/primitiveTactics.ml		diff \| blob \| history
helm/software/components/tactics/primitiveTactics.mli		diff \| blob \| history
helm/software/components/tactics/proofEngineHelpers.ml		diff \| blob \| history
helm/software/components/tactics/proofEngineHelpers.mli		diff \| blob \| history
helm/software/components/tactics/proofEngineReduction.ml		diff \| blob \| history
helm/software/components/tactics/proofEngineStructuralRules.ml		diff \| blob \| history
helm/software/components/tactics/reductionTactics.ml		diff \| blob \| history
helm/software/components/tactics/setoids.ml		diff \| blob \| history
helm/software/components/tactics/universe.ml		diff \| blob \| history
helm/software/components/tactics/variousTactics.ml		diff \| blob \| history
helm/software/matita/matitaScript.ml		diff \| blob \| history

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

RSS Atom