From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 9 Feb 2010 07:20:55 +0000 (+0000)
Subject: Added a count_occurrences function.
X-Git-Tag: make_still_working~3048
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=213cd54a013aca96640d611f2c6c65f7f8e24f4c;p=helm.git

Added a count_occurrences function.
---

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index b110d0651..9c96469e5 100644
--- 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
diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli
index 01c522ba0..702f8fc19 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.mli
+++ b/helm/software/components/ng_kernel/nCicUntrusted.mli
@@ -42,4 +42,4 @@ val apply_subst_context : fix_projections:bool ->
 val apply_subst_metasenv : NCic.substitution -> NCic.metasenv -> NCic.metasenv
 
 val count_occurrences :
-    subst:NCic.substitution -> NCic.context -> int -> NCic.term -> int
+    subst:NCic.substitution -> int -> NCic.term -> int