Thanks to Guarrigue, code for Serializer functor simplified using

[helm.git] / matita / components / ng_refiner / nCicRefiner.ml

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index a59a6fd359109202b3c8aed7c39efcaf1c6e3339..550c75e9382c4ec9173f76d1da3d9428f28644d0 100644 (file)
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -505,13 +505,14 @@ and try_coercions status
   (* we try with a coercion *)
   let rec first exc = function
   | [] ->   
-     let expty =
-      match expty with
-         `Type expty -> status#ppterm ~metasenv ~subst ~context expty
-       | `Sort -> "[[sort]]"
-       | `Prod -> "[[prod]]" in
       pp (lazy "WWW: no more coercions!");      
-      raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
+      raise (wrap_exc (lazy
+       let expty =
+        match expty with
+           `Type expty -> status#ppterm ~metasenv ~subst ~context expty
+         | `Sort -> "[[sort]]"
+         | `Prod -> "[[prod]]" in
+         (localise orig_t, Printf.sprintf
         "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
         (status#ppterm ~metasenv ~subst ~context t)
         (status#ppterm ~metasenv ~subst ~context infty)
@@ -915,7 +916,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