Added a count_occurrences function.

[helm.git] / helm / software / components / ng_kernel / nCicUntrusted.ml

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index b110d0651adff6d6afd61978a43d8589fe1f6900..9c96469e55053487f64026c66184648f9a0d2684 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -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