X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=82f7cef800fc8874467d972dd40f2c29bb0d22e2;hb=cb11de1c61f0b61935b1c6c1832deacb49f7b5bd;hp=9c96469e55053487f64026c66184648f9a0d2684;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_kernel/nCicUntrusted.ml b/matita/components/ng_kernel/nCicUntrusted.ml
index 9c96469e5..82f7cef80 100644
--- a/matita/components/ng_kernel/nCicUntrusted.ml
+++ b/matita/components/ng_kernel/nCicUntrusted.ml
@@ -317,7 +317,7 @@ 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 -> ()
+    | C.Rel _m -> ()
     | C.Implicit _ -> ()
     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
     | C.Meta (mno,(s,l)) ->
@@ -334,3 +334,17 @@ let count_occurrences ~subst 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
+;;