]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_refiner/nDiscriminationTree.ml
collapse applications with a Match as head while indexing
[helm.git] / matita / components / ng_refiner / nDiscriminationTree.ml
index 3c30ce0029749d06c70b7de8e01623dc96701fd9..4d746ad8baf2f74fa3ff83c4936f08d214c45891 100644 (file)
@@ -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]