X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnDiscriminationTree.ml;h=4d746ad8baf2f74fa3ff83c4936f08d214c45891;hb=3f57ed2589601e79478c85d74708d8ebdec2cf20;hp=50c3bd208d2b1c4465b0da542a9ecdbe8a72f803;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_refiner/nDiscriminationTree.ml b/matita/components/ng_refiner/nDiscriminationTree.ml
index 50c3bd208..4d746ad8b 100644
--- a/matita/components/ng_refiner/nDiscriminationTree.ml
+++ b/matita/components/ng_refiner/nDiscriminationTree.ml
@@ -65,13 +65,14 @@ 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]
     | NCic.Appl (hd::tl) ->
        aux (List.length tl) depth hd @ 
        List.flatten (List.map (aux 0 (depth+1)) tl)
-    | NCic.Lambda _ | NCic.Prod _ -> [Variable]
+    | NCic.Lambda _ -> [Variable]
         (* I think we should CicSubstitution.subst Implicit t *)
     | NCic.LetIn _ -> [Variable] (* z-reduce? *)
     | NCic.Meta _ | NCic.Implicit _ -> assert (arity = 0); [Variable]
@@ -79,7 +80,9 @@ let path_string_of t =
     | NCic.Sort (NCic.Prop) -> assert (arity=0); [Proposition]
     | NCic.Sort _ -> assert (arity=0); [Datatype]
     | NCic.Const (u) -> [Constant (u, arity)]
-    | NCic.Match _ -> [Dead]
+    (* Prod is used for coercions to funclass, ?->?       *)
+    (*  so it should not be unifiable with any other term *)
+    | NCic.Match _ | NCic.Prod _ -> [Dead] 
   in 
   aux 0 0 t
 ;;