X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=945916153c877ac485e955e6c2b09d28ef6cf838;hb=8a5c30a914d7ff665218b31853c6fb4bcf58aa08;hp=0523ef8b202fae7e1c406b8758e5b8be78651581;hpb=d7aca3eacb4bd8dc56223098f92e5370c82f92ff;p=helm.git

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index 0523ef8b2..945916153 100644
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -234,7 +234,7 @@ let rec typeof (status:#NCicCoercion.status)
     (*D*)in outside true; rc with exc -> outside false; raise exc
   in
   let rec typeof_aux metasenv subst context expty = 
-    fun t as orig -> 
+    fun (t as orig) -> 
     (*D*)inside 'R'; try let rc = 
     pp (lazy (status#ppterm ~metasenv ~subst ~context t ^ " ::exp:: " ^
        match expty with `XTSort -> "Any sort" | `XTInd -> "Any (co)inductive type"
@@ -551,7 +551,7 @@ and try_coercions status
   | [] ->   
       pp (lazy "WWW: no more coercions!");
       raise (wrap_exc (lazy
-       let expty =
+       (let expty =
         match expty with
            `XTSome expty -> status#ppterm ~metasenv ~subst ~context expty
          | `XTSort -> "[[sort]]"
@@ -561,7 +561,7 @@ and try_coercions status
         "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)
-        expty)) exc)
+        expty))) exc)
   | (_,metasenv, newterm, newtype, meta)::tl ->
       try 
           pp (lazy("K=" ^ status#ppterm ~metasenv ~subst ~context newterm));