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"

diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml
index 96efe2e3cb7ff5f72442593effbc70d461452680..8d53495bff9024f6adc8247f739da57d83470829 100644 (file)
--- a/components/cic_unification/cicMetaSubst.ml
+++ b/components/cic_unification/cicMetaSubst.ml
@@ -98,7 +98,6 @@ let rec deref subst =
 let lookup_subst = CicUtil.lookup_subst
 ;;
 
-
 (* clean_up_meta take a metasenv and a term and make every local context
 of each occurrence of a metavariable consistent with its canonical context, 
 with respect to the hidden hipothesis *)
@@ -749,15 +748,14 @@ debug_print(lazy (sprintf
             l))))
       in
        if
-        (*CSC: WARNING: if we are working up to reduction (I do not think so),
-          the following test should be replaced with "all the terms in l are
-          meta-closed" *)
-        not
-         (List.exists (function Some (Cic.Meta _) -> true | _ -> false ) l)
+         List.exists
+          (function
+              Some t -> CicUtil.is_meta_closed (apply_subst subst t)
+            | None -> true) l
        then
-        raise (MetaSubstFailure msg)
-       else
         raise (Uncertain msg)
+       else
+        raise (MetaSubstFailure msg)
    in
    let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
     res, metasenv, subst
@@ -914,4 +912,3 @@ let fpp_gen ppf s =
 let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
 let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
 let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv)
-

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index be4014507355ab62e4d319fa115074b9aee1b552..8ae5964c9cf209a8ba43ea65a1c9efcbd0329b40 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -1510,7 +1510,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
     in
     (* first we check if we are in the simple case of a meta closed term *)
     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
-     if CicUtil.is_meta_closed hetype then
+     if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
       (* this optimization is to postpone fix_arity (the most common case)*)
       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
      else