More aggressive politic for non localized terms: an assert false!

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 661d5c34c94c76a5c2db65846b4ce5cd738f990d..18ed5a0761d5ef5bd8fa87cd4ccad0c171ba9ff3 100644 (file)
--- 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 ->