X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_refiner%2FnDiscriminationTree.ml;h=531f7642832338f5d1285a060ae062924f8d84dc;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hp=50c3bd208d2b1c4465b0da542a9ecdbe8a72f803;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/ng_refiner/nDiscriminationTree.ml b/matitaB/components/ng_refiner/nDiscriminationTree.ml
index 50c3bd208..531f76428 100644
--- a/matitaB/components/ng_refiner/nDiscriminationTree.ml
+++ b/matitaB/components/ng_refiner/nDiscriminationTree.ml
@@ -65,6 +65,7 @@ let ppelem = function
 let path_string_of t =
   let rec aux arity depth = function
     | NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
+    | NCic.Appl (NCic.Match _::_) -> [Dead]
     | 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]