From 7bf186f42e827e6e4112eba7ae5ca3e727f59026 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 11 Jan 2012 10:45:07 +0000 Subject: [PATCH] Fixes r11788 (partial, thus broken commit). --- matita/components/ng_refiner/nCicRefiner.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml index a59a6fd35..563fe3928 100644 --- a/matita/components/ng_refiner/nCicRefiner.ml +++ b/matita/components/ng_refiner/nCicRefiner.ml @@ -915,7 +915,7 @@ and force_to_sort status metasenv subst context t orig_t localise ty = " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in let ty = NCicReduction.whd status ~subst context ty in let exn = - if NCicUnification.could_reduce ty then + if NCicUnification.could_reduce status ~subst context ty then Uncertain msg else RefineFailure msg -- 2.39.2