From 040489c7decbea06f923332fee132165b7097145 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 May 2011 11:57:17 +0000 Subject: [PATCH] Prod indexed as Dead, that is equal only to itself, instead of Variable that is equal to anything --- matita/components/ng_refiner/nDiscriminationTree.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 ;; -- 2.39.2