]> matita.cs.unibo.it Git - helm.git/commit
- removed unwind: every substitution is now _not_ unwinded
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 2 Feb 2004 16:14:56 +0000 (16:14 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 2 Feb 2004 16:14:56 +0000 (16:14 +0000)
commit4ce27bd72e72474d4d6654898faaa5a583dd6365
treed67fce97371ae6ab960a0d3a19de6d4adfe4bb08
parentf4b9cc6f689b52e0408ac3231ba2a480d71216fb
- removed unwind: every substitution is now _not_ unwinded
- removed extra metasenv argument from all kernel proxies
- added kernel proxy: subst (for CicSubstitution.subst)
- added pretty printer ppterm
helm/ocaml/cic_unification/cicMetaSubst.ml
helm/ocaml/cic_unification/cicMetaSubst.mli