]> matita.cs.unibo.it Git - helm.git/commit
New handling of substitution:
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 1 Jul 2004 14:12:30 +0000 (14:12 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 1 Jul 2004 14:12:30 +0000 (14:12 +0000)
commit7ec7262cfa317c1962164350361f82a56c5d1826
tree88e7911f911b95c25da58415bba711aee3a46a6a
parentda49d2dca60a85abe54e0e549b290fa28a8127ba
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
helm/ocaml/cic_omdoc/doubleTypeInference.ml
helm/ocaml/cic_omdoc/eta_fixing.ml
helm/ocaml/cic_proof_checking/cicTypeChecker.ml
helm/ocaml/cic_unification/.depend
helm/ocaml/cic_unification/Makefile
helm/ocaml/cic_unification/cicMetaSubst.ml
helm/ocaml/cic_unification/cicMetaSubst.mli
helm/ocaml/cic_unification/cicMkImplicit.ml
helm/ocaml/cic_unification/cicMkImplicit.mli
helm/ocaml/cic_unification/cicRefine.ml
helm/ocaml/cic_unification/cicUnification.ml
helm/ocaml/tactics/primitiveTactics.ml
helm/ocaml/tactics/proofEngineHelpers.ml
helm/ocaml/tactics/variousTactics.ml