X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnDiscriminationTree.ml;h=fff8b67699c6d5388dfa811995d30a686a5aff84;hb=2dd6e8f11fa3ac2995f326ecb742d9b4e8948fce;hp=bd64cfe5d5a036b2ad0e69e0356c52a2718384af;hpb=eaf5880ed69963b3ad37cb1f8a1fd48b2918e58b;p=helm.git

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
index bd64cfe5d..fff8b6769 100644
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -51,13 +51,15 @@ let ppelem = function
   | Dead -> "Dead"
 ;;
 
-let path_string_of =
-  let rec aux arity = function
+let path_string_of t =
+  let rec aux arity depth = function
     | NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
     | NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
     | NCic.Appl [] -> assert false
+    | NCic.Appl l when depth > 10 || List.length l > 50 -> [Variable]
     | NCic.Appl (hd::tl) ->
-        aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) 
+       aux (List.length tl) depth hd @ 
+       List.flatten (List.map (aux 0 (depth+1)) tl)
     | NCic.Lambda _ | NCic.Prod _ -> [Variable]
         (* I think we should CicSubstitution.subst Implicit t *)
     | NCic.LetIn _ -> [Variable] (* z-reduce? *)
@@ -68,7 +70,7 @@ let path_string_of =
     | NCic.Const (NReference.Ref (u,_)) -> [Constant (u, arity)]
     | NCic.Match _ -> [Dead]
   in 
-    aux 0
+  aux 0 0 t
 ;;
 
 let compare e1 e2 =