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

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

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Wed, 15 Jun 2005 10:55:08 +0000 (10:55 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Wed, 15 Jun 2005 10:55:08 +0000 (10:55 +0000)
commit	358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3
tree	06cef375f9af35ac0d0a54efa28ff4d4cb36e407	tree \| snapshot
parent	53ee2f5095adadffcafb40e436d23dc330d3bd87	commit \| diff

Big commit and major code clean-up:
1. added a refine function for objects
2. added a disambiguation function for objects
3. MatitaEngine now uses the disambiguation function for objects
4. added CicTypeChecker.typecheck_obj to typecheck an object and add it
to the environment

31 files changed:

helm/matita/matita.conf.xml	[new file with mode: 0644]	blob
helm/matita/matita.txt		diff \| blob \| history
helm/matita/matitaDisambiguator.ml		diff \| blob \| history
helm/matita/matitaEngine.ml		diff \| blob \| history
helm/matita/matitaEngine.mli		diff \| blob \| history
helm/matita/matitaSync.ml		diff \| blob \| history
helm/matita/matitaSync.mli		diff \| blob \| history
helm/matita/tests/match.ma		diff \| blob \| history
helm/ocaml/cic/cicUtil.mli		diff \| blob \| history
helm/ocaml/cic_disambiguation/cicTextualParser2.ml		diff \| blob \| history
helm/ocaml/cic_disambiguation/cicTextualParser2.mli		diff \| blob \| history
helm/ocaml/cic_disambiguation/disambiguate.ml		diff \| blob \| history
helm/ocaml/cic_disambiguation/disambiguate.mli		diff \| blob \| history
helm/ocaml/cic_disambiguation/disambiguateTypes.ml		diff \| blob \| history
helm/ocaml/cic_disambiguation/disambiguateTypes.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicElim.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicElim.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicEnvironment.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicEnvironment.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicRecord.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicRecord.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicTypeChecker.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicTypeChecker.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/utilities/create_environment.ml		diff \| blob \| history
helm/ocaml/cic_transformations/tacticAst.ml		diff \| blob \| history
helm/ocaml/cic_transformations/tacticAstPp.ml		diff \| blob \| history
helm/ocaml/cic_transformations/tacticAstPp.mli		diff \| blob \| history
helm/ocaml/cic_unification/cicMkImplicit.ml		diff \| blob \| history
helm/ocaml/cic_unification/cicMkImplicit.mli		diff \| blob \| history
helm/ocaml/cic_unification/cicRefine.ml		diff \| blob \| history
helm/ocaml/cic_unification/cicRefine.mli		diff \| blob \| history

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

RSS Atom