X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=325ced5c436e9009c5072993ade330af1f0045fa;hb=1ac7951d70bb5c850697643e3df303290f69bc74;hp=6dfa7afee01c328cdbfa01d0e314fabee8d070f4;hpb=6120c5ba6c24eeeb2f932ba7e247a751c4216134;p=helm.git diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml index 6dfa7afee..325ced5c4 100644 --- a/matita/components/ng_refiner/nCicUnification.ml +++ b/matita/components/ng_refiner/nCicUnification.ml @@ -140,7 +140,7 @@ let rec could_reduce status ~subst context = | C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args) when List.length args > recno -> let t = NCicReduction.whd status ~subst context (List.nth args recno) in - could_reduce status subst context t + could_reduce status ~subst context t | C.Match (_,_,he,_) -> let he = NCicReduction.whd status ~subst context he in could_reduce status ~subst context he