From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 11 Jan 2012 10:45:07 +0000 (+0000)
Subject: Fixes r11788 (partial, thus broken commit).
X-Git-Tag: make_still_working~1980
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7bf186f42e827e6e4112eba7ae5ca3e727f59026;p=helm.git

Fixes r11788 (partial, thus broken commit).
---

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