\ldots are now used in nelim and ncases

[helm.git] / helm / software / components / ng_refiner / nCicMetaSubst.ml

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index a445d16be4cf6a99a8937c6026c322672454854c..9cc6ac67c755c16e4208413f1cd7565859c64557 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -215,8 +215,6 @@ let rec flexible_arg subst = function
   | _ -> false
 ;;
 
-let flexible subst l = List.exists (flexible_arg subst) l;;
-
 let in_scope_tag  = "tag:in_scope" ;;
 let out_scope_tag_prefix = "tag:out_scope:" 
 let out_scope_tag n = out_scope_tag_prefix ^ string_of_int n ;;
@@ -435,7 +433,7 @@ let delift ~unify metasenv subst context n l t =
       let lc = NCicUtils.expand_local_context lc in
       let l = List.map (NCicSubstitution.lift shift) lc in
        if
-        List.exists (fun t-> NCicUntrusted.metas_of_term subst context t = []) l
+        List.exists (fun t-> NCicUntrusted.metas_of_term subst context t <> [])l
        then
         raise (Uncertain msg)
        else