X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=f01ecf785ed8524f5002d6c3f6e08610a617bdbb;hb=acd31bfb9537bd32781404241c80bd0ebf88e3b1;hp=e1c1e91cee28838f92891ac72c3e335a65a7ab7a;hpb=cf3635c0830661f59d16339cd7fc9c3b948fcbc8;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index e1c1e91ce..f01ecf785 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 open Printf
 
 exception RefineFailure of string Lazy.t;;
@@ -851,7 +853,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
 
   and  avoid_double_coercion subst metasenv ugraph t ty = 
     match t with
-    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when 
+    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when 
       CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
           let source_carr = CoercGraph.source_of c2 in
           let tgt_carr = CicMetaSubst.apply_subst subst ty in
@@ -1087,7 +1089,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                          let c_s = carr s subst context in 
                          CoercGraph.look_for_coercion c_hety c_s, c_s
                        in
-                       match coer with
+                       (match coer with
                        | CoercGraph.NoCoercion 
                        | CoercGraph.NotHandled _ ->
                            enrich localization_tbl hete
@@ -1115,7 +1117,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                               subst metasenv ugraph 
                                 (Cic.Appl[c;hete]) tgt_carr
                            in
-                            newt, subst, metasenv, ugraph
+                            newt, subst, metasenv, ugraph)
+                     | exn ->
+                        enrich localization_tbl hete
+                         ~f:(fun _ ->
+                           (lazy ("The term " ^
+                             CicMetaSubst.ppterm_in_context subst hete
+                              context ^ " has type " ^
+                             CicMetaSubst.ppterm_in_context subst hety
+                              context ^ " but is here used with type " ^
+                             CicMetaSubst.ppterm_in_context subst s context
+                              (* "\nReason: " ^ Lazy.force e*)))) exn
                    in
                    let coerced_args,metasenv',subst',t',ugraph2 =
                      eat_prods metasenv subst context
@@ -1321,7 +1333,9 @@ let typecheck metasenv uri obj ~localization_tbl =
          let metasenv,ugraph,cl' =
           List.fold_right
            (fun (name,ty) (metasenv,ugraph,res) ->
-             let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
+             let ty =
+              CicTypeChecker.debrujin_constructor
+               ~cb:(relocalize localization_tbl) uri typesno ty in
              let ty',_,metasenv,ugraph =
               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
              let ty' = undebrujin uri typesno tys ty' in