From 511421f12dd04547bbf1206470e5d39237673429 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 1 Mar 2010 18:07:54 +0000 Subject: [PATCH] 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. --- helm/software/components/ng_refiner/nCicUnification.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index c7b487461..1f03755ff 100644 --- 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 = -- 2.39.2