Fixed a bug in the unification, which prevented some reduction steps from being

performed in the case "match vs. match", when the types of the matching term
were not the same. The procedure used to always raise an Uncertain exception,
while in many cases the good choice would be to raise KeepReducing. This caused
the nnormalize tactic to fail with an error in some cases.

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index c7b487461963a179bd6333232cefb7ce13385bbf..1f03755ffbd9cde673cc3be5c9cbeffe9809d23f 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -619,7 +619,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
              metasenv, subst
 
        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
-          C.Match (ref2,outtype2,term2,pl2)) ->
+          C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
            let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
            let _,_,ty,_ = List.nth itl tyno in
            let rec remove_prods ~subst context ty = 
@@ -635,9 +635,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
              | C.Sort C.Prop -> true
              | _ -> false 
            in
-           if not (Ref.eq ref1 ref2) then 
+           (* if not (Ref.eq ref1 ref2) then 
              raise (Uncertain (mk_msg metasenv subst context t1 t2))
-           else
+           else*)
              let metasenv, subst = 
               unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
              let metasenv, subst =