From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 17 Nov 2011 23:14:26 +0000 (+0000)
Subject: collapse applications with a Match as head while indexing
X-Git-Tag: make_still_working~2096
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dba584374a26ef04c53306c89e5567e637e6553e;p=helm.git

collapse applications with a Match as head while indexing
---

diff --git a/matita/components/ng_refiner/nDiscriminationTree.ml b/matita/components/ng_refiner/nDiscriminationTree.ml
index 3c30ce002..4d746ad8b 100644
--- a/matita/components/ng_refiner/nDiscriminationTree.ml
+++ b/matita/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]