]> matita.cs.unibo.it Git - helm.git/commit
1. is_meta_closed should be applied only to terms on which a substitution
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 25 Oct 2006 17:42:45 +0000 (17:42 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 25 Oct 2006 17:42:45 +0000 (17:42 +0000)
commit237e58b77eda53354d9621e3e2f684c30f7da763
treee41329636008a7bc2b2ab95e5547068d476aa404
parent3bfe4a4442b5cd52173957b54e6ef76b98bce367
1. is_meta_closed should be applied only to terms on which a substitution
   has already been applied. Fixed here and there.
   Note: it is not possible to add a subst parameter to is_meta_closed since
   the function is declared in cic/CicUtil and it is used where the unification
   is not available (e.g. in whelp and library)
2. known (but never verified before) bug fixed: delifting should fail
   (instead of raising Uncertain) iff the local context is not meta_closed.
   The test used to be "does not contain a Meta"
components/cic_unification/cicMetaSubst.ml
components/cic_unification/cicRefine.ml