From 5f87c295e57d5c5ef9bcb13d71f19b24642355be Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 10 Jun 2008 15:32:22 +0000 Subject: [PATCH] relevance check for Match --- .../components/ng_kernel/nCicReduction.ml | 22 +++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 20a573c5d..61bb201b7 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -13,6 +13,7 @@ module C = NCic module Ref = NReference +module E = NCicEnvironment module type Strategy = sig type stack_term @@ -231,14 +232,27 @@ let are_convertible ?(subst=[]) get_relevance = tl1 tl2 true relevance with Invalid_argument _ -> false) - | (C.Match (ref1,outtype1,term1,pl1), - C.Match (ref2,outtype2,term2,pl2)) -> + | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1), + C.Match (ref2,outtype2,term2,pl2)) -> + let _,_,itl,_,_ = E.get_checked_indtys ref1 in + let _,_,ty,_ = List.nth itl tyno in + let rec remove_prods ~subst context ty = + let ty = whd ~subst context ty in + match ty with + | C.Sort _ -> ty + | C.Prod (name,so,ta) -> remove_prods ~subst ((name,(C.Decl so))::context) ta + | _ -> assert false + in + let is_prop = + match remove_prods ~subst [] ty with + | C.Sort C.Prop -> true + | _ -> false + in Ref.eq ref1 ref2 && aux test_eq_only context outtype1 outtype2 && - aux test_eq_only context term1 term2 && + (is_prop || aux test_eq_only context term1 term2) && (try List.for_all2 (aux test_eq_only context) pl1 pl2 with Invalid_argument _ -> false) - | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (_,_) -> false in -- 2.39.2