relevance check for Match

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 20a573c5dd755a824247a7f512f3cf5f46329b48..61bb201b7f685e0e6c3bf615c4b4406aba719cb5 100644 (file)
--- 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