X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=18ed5a0761d5ef5bd8fa87cd4ccad0c171ba9ff3;hb=4fb01ad004146d7563e14dc4901731eb8010f640;hp=6d28ca1779972be28c6619ad7f0cd5bed8be78b5;hpb=e674cb67c1f52747111fa3935d1523e1af8222f5;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 6d28ca177..18ed5a076 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -43,16 +43,20 @@ in profiler.HExtlib.profile foo ()
     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
 ;;
 
-let enrich loc f exn =
+let enrich localization_tbl t f exn =
  let exn' =
   match exn with
      RefineFailure msg -> RefineFailure (f msg)
    | Uncertain msg -> Uncertain (f msg)
-   | _ -> assert false
+   | _ -> assert false in
+ let loc =
+  try
+   Cic.CicHash.find localization_tbl t
+  with Not_found ->
+   (* prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); *)
+   assert false
  in
-  match loc with
-     None -> raise exn'
-   | Some loc -> raise (HExtlib.Localized (loc,exn'))
+  raise (HExtlib.Localized (loc,exn'))
 
 let relocalize localization_tbl oldt newt =
  try
@@ -1023,9 +1027,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                             CicMetaSubst.ppterm_in_context subst s context
                              (* "\nReason: " ^ Lazy.force e*))
                           in
-                           enrich 
-                            (try Some (Cic.CicHash.find localization_tbl hete) with Not_found -> prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm hete); None)
-                            msg exn
+                           enrich localization_tbl hete msg exn
                        | CoercGraph.NotMetaClosed -> 
                            raise (Uncertain (lazy "Coercions on meta"))
                        | CoercGraph.SomeCoercion c -> 
@@ -1122,7 +1124,6 @@ let map_first_n n start f g l =
    
 (*CSC: this is a very rough approximation; to be finished *)
 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
-  let number_of_types = List.length tys in
   let subst,metasenv,ugraph,tys = 
     List.fold_right
       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->