X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=6f1d8718ae02d8c1b0998c1664c498b4959735f4;hb=8a5c30a914d7ff665218b31853c6fb4bcf58aa08;hp=553e1e6716654ebcc9a62de0c6d561b69b2bbdb5;hpb=d7aca3eacb4bd8dc56223098f92e5370c82f92ff;p=helm.git diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml index 553e1e671..6f1d8718a 100644 --- a/matita/components/ng_refiner/nCicUnification.ml +++ b/matita/components/ng_refiner/nCicUnification.ml @@ -276,7 +276,7 @@ let tipify status exc metasenv subst context t ty = let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in let metasenv = NCicUntrusted.replace_in_metasenv n - (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty) + (fun (attrs,cc,_) -> NCicUntrusted.set_kind `IsType attrs, cc, ty) metasenv in metasenv,subst,false @@ -290,7 +290,7 @@ let tipify status exc metasenv subst context t ty = let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in let subst = NCicUntrusted.replace_in_subst n - (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty) + (fun (attrs,cc,bo,_)->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty) subst in optimize_meta metasenv subst (NCicSubstitution.subst_meta status lc bo)) @@ -557,8 +557,7 @@ and fo_unif0 during_delift status swap test_eq_only metasenv subst context (norm i | NCic.Meta (i,_) -> (metasenv, subst), i | _ -> - raise (UnificationFailure (lazy "Locked term vs non - flexible term; probably not saturated enough yet!")) + raise (UnificationFailure (lazy "Locked term vs non flexible term; probably not saturated enough yet!")) in let t1 = NCicReduction.whd status ~subst context t1 in let j, lj =