X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnDiscriminationTree.ml;h=3c30ce0029749d06c70b7de8e01623dc96701fd9;hb=44ef57f5e371159a7900fe8d50db1c84a66151cd;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..3c30ce002 100644
--- a/matita/components/ng_refiner/nDiscriminationTree.ml
+++ b/matita/components/ng_refiner/nDiscriminationTree.ml
@@ -71,7 +71,7 @@ let path_string_of t =
     | 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 +79,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
 ;;