X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=633ecea576540e80ed8786eef5916c6bcd783c88;hb=889815067d64e081eb90ea1a792890c2ad4e511c;hp=dc26794a1a096cb4f9575e93cf9e826cbe83989a;hpb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index dc26794a1..633ecea57 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -177,7 +177,7 @@ let apply_subst subst context t =
        let t = NCicSubstitution.subst_meta lc t in
         apply_subst subst () t
       with
-       Not_found ->
+       NCicUtils.Subst_not_found j when j = i ->
         match lc with
            _,NCic.Irl _ -> NCic.Meta (i,lc)
          | n,NCic.Ctx l ->
@@ -209,42 +209,3 @@ let rec apply_subst_metasenv subst = function
       (i,(name,apply_subst_context subst ctx,apply_subst subst ctx ty)) ::
          apply_subst_metasenv subst tl
 ;;
-
-let height_of_term tl =
- let h = ref 0 in
- let get_height (NReference.Ref (uri,_)) =
-  let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in
-   height in
- let rec aux =
-  function
-     NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
-   | NCic.Meta _ -> ()
-   | NCic.Rel _
-   | NCic.Sort _ -> ()
-   | NCic.Implicit _ -> assert false
-   | NCic.Const nref -> h := max !h (get_height nref)
-   | NCic.Prod (_,t1,t2)
-   | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
-   | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
-   | NCic.Appl l -> List.iter aux l
-   | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
- in
-  List.iter aux tl;
-  1 + !h
-;;
-
-let height_of_obj_kind uri =
- function
-    NCic.Inductive _
-  | NCic.Constant (_,_,None,_,_)
-  | NCic.Fixpoint (false,_,_) -> 0
-  | NCic.Fixpoint (true,ifl,_) ->
-     let iflno = List.length ifl in
-      height_of_term
-       (List.fold_left
-        (fun l (_,_,_,ty,bo) ->
-          let bo = NCicTypeChecker.debruijn uri iflno [] bo in
-           ty::bo::l
-       ) [] ifl)
-  | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty]
-;;