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

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

author	Stefano Zacchiroli <zack@upsilon.cc>
	Thu, 1 Jul 2004 14:12:30 +0000 (14:12 +0000)
committer	Stefano Zacchiroli <zack@upsilon.cc>
	Thu, 1 Jul 2004 14:12:30 +0000 (14:12 +0000)
commit	7ec7262cfa317c1962164350361f82a56c5d1826
tree	88e7911f911b95c25da58415bba711aee3a46a6a	tree \| snapshot
parent	da49d2dca60a85abe54e0e549b290fa28a8127ba	commit \| diff

New handling of substitution:
- splitted metasenv from substitution
- substitution enriched with canonical context information for
checking_metasenv_consistency

15 files changed:

helm/ocaml/cic_omdoc/cic2acic.ml		diff \| blob \| history
helm/ocaml/cic_omdoc/doubleTypeInference.ml		diff \| blob \| history
helm/ocaml/cic_omdoc/eta_fixing.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicTypeChecker.ml		diff \| blob \| history
helm/ocaml/cic_unification/.depend		diff \| blob \| history
helm/ocaml/cic_unification/Makefile		diff \| blob \| history
helm/ocaml/cic_unification/cicMetaSubst.ml		diff \| blob \| history
helm/ocaml/cic_unification/cicMetaSubst.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/cicUnification.ml		diff \| blob \| history
helm/ocaml/tactics/primitiveTactics.ml		diff \| blob \| history
helm/ocaml/tactics/proofEngineHelpers.ml		diff \| blob \| history
helm/ocaml/tactics/variousTactics.ml		diff \| blob \| history

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

RSS Atom