X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=022482b0a9e60c44e20398d586b74bd9ddaa9e2a;hb=d3a143f3edce2a255c449526e0ecf85435a6bad4;hp=b110d0651adff6d6afd61978a43d8589fe1f6900;hpb=2da35c1dc1aff5f852886ac64d641774f2f187cf;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index b110d0651..022482b0a 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -271,9 +271,9 @@ let rec replace_in_subst i f = function
   | (j,e)::tl when j=i -> (i,f e) :: tl
   | x::tl -> x :: replace_in_subst i f tl
 ;;
-          
+
 let set_kind newkind attrs = 
-  newkind :: List.filter (fun x -> not (is_kind x)) attrs 
+  (newkind :> NCic.meta_attr) :: List.filter (fun x -> not (is_kind x)) attrs 
 ;;
 
 let max_kind k1 k2 = 
@@ -313,15 +313,12 @@ let sort_metasenv subst (m : NCic.metasenv) =
   (MS.topological_sort m (relations_of_menv subst m) : NCic.metasenv)
 ;;
 
-let count_occurrences ~subst context n t = 
+let count_occurrences ~subst n t = 
   let occurrences = ref 0 in
   let rec aux k _ = function
     | C.Rel m when m = n+k -> incr occurrences
-    | C.Rel m ->
-        (try match List.nth context (m-1-k) with
-          | _,C.Def (bo,_) -> aux (n-m) () bo
-          | _ -> ()
-         with Failure _ -> assert false)
+    | C.Rel _m -> ()
+    | C.Implicit _ -> ()
     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
     | C.Meta (mno,(s,l)) ->
          (try
@@ -337,3 +334,17 @@ let count_occurrences ~subst context n t =
    aux 0 () t;
    !occurrences
 ;;
+
+exception Found_variable
+
+let looks_closed t = 
+  let rec aux k _ = function
+    | C.Rel m when k < m -> raise Found_variable
+    | C.Rel _m -> ()
+    | C.Implicit _ -> ()
+    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
+    | C.Meta _ -> raise Found_variable
+    | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t
+  in
+  try aux 0 () t; true with Found_variable -> false
+;;