From 7c8bd0b1b479f162ba63e0e2eeb27bc2e7d97123 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 17 Nov 2011 23:14:39 +0000 Subject: [PATCH] collapse applications with a Match as head while indexing --- matitaB/components/ng_refiner/nDiscriminationTree.ml | 1 + 1 file changed, 1 insertion(+) 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] -- 2.39.2