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

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 239db16cf11560a552531c03ee2aebe83fa2be1d..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
@@ -207,7 +211,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
     let module C = Cic in
     let module S = CicSubstitution in
     let module U = UriManager in
-    (* this stops on binders, so we have to call it every time *)
+     let (t',_,_,_,_) as res =
       match t with
           (*    function *)
           C.Rel n ->
@@ -392,7 +396,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                    let x',ty,subst',metasenv',ugraph1 =
                      type_of_aux subst metasenv context x ugraph
                    in
-                    relocalize localization_tbl x x';
                     (x', ty)::res,subst',metasenv',ugraph1
                 ) tl ([],subst',metasenv',ugraph1)
             in
@@ -783,6 +786,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               fl_ty' fl_bo' fl 
             in
               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
+     in
+      relocalize localization_tbl t t';
+      res
 
   (* check_metasenv_consistency checks that the "canonical" context of a
      metavariable is consitent - up to relocation via the relocation list l -
@@ -1021,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 -> 
@@ -1120,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) ->