From: Andrea Asperti 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