More error messages localized.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 18ed5a0761d5ef5bd8fa87cd4ccad0c171ba9ff3..35c92a4139210085c47084ca153e73851c20b703 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -43,7 +43,7 @@ in profiler.HExtlib.profile foo ()
     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
 ;;
 
-let enrich localization_tbl t f exn =
+let enrich localization_tbl t ?(f = fun msg -> msg) exn =
  let exn' =
   match exn with
      RefineFailure msg -> RefineFailure (f msg)
@@ -53,7 +53,7 @@ let enrich localization_tbl t f exn =
   try
    Cic.CicHash.find localization_tbl t
   with Not_found ->
-   (* prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); *)
+   prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
    assert false
  in
   raise (HExtlib.Localized (loc,exn'))
@@ -228,9 +228,13 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                        (S.lift n bo) ugraph 
                      in
                       t,ty,subst,metasenv,ugraph
-                 | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis"))
+                 | None ->
+                    enrich localization_tbl t
+                     (RefineFailure (lazy "Rel to hidden hypothesis"))
              with
-                 _ -> raise (RefineFailure (lazy "Not a close term")))
+              _ ->
+               enrich localization_tbl t
+                (RefineFailure (lazy "Not a close term")))
         | C.Var (uri,exp_named_subst) ->
             let exp_named_subst',subst',metasenv',ugraph1 =
               check_exp_named_subst 
@@ -279,11 +283,23 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
             let te',inferredty,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' context te ugraph1
             in
-                 let subst''',metasenv''',ugraph3 =
-                   fo_unif_subst subst'' context metasenv'' 
-                     inferredty ty' ugraph2
-                 in
-                   C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
+             (try
+               let subst''',metasenv''',ugraph3 =
+                 fo_unif_subst subst'' context metasenv'' 
+                   inferredty ty' ugraph2
+               in
+                C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
+              with
+               exn ->
+                enrich localization_tbl t
+                 ~f:(fun _ ->
+                   lazy ("The term " ^
+                    CicMetaSubst.ppterm_in_context subst'' te
+                     context ^ " has type " ^
+                    CicMetaSubst.ppterm_in_context subst'' inferredty
+                     context ^ " but is here used with type " ^
+                    CicMetaSubst.ppterm_in_context subst'' ty context)) exn
+             )
         | C.Prod (name,s,t) ->
             let carr t subst context = CicMetaSubst.apply_subst subst t in
             let coerce_to_sort 
@@ -313,10 +329,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                   (match boh with
                   | CoercGraph.NoCoercion
                   | CoercGraph.NotHandled _ -> 
-                     raise
+                     enrich localization_tbl s
                       (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
                   | CoercGraph.NotMetaClosed -> 
-                     raise
+                     enrich localization_tbl s
                       (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
                   | CoercGraph.SomeCoercion c -> 
                       Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
@@ -1018,7 +1034,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                        match coer with
                        | CoercGraph.NoCoercion 
                        | CoercGraph.NotHandled _ ->
-                          let msg e =
+                          let msg _e =
                            lazy ("The term " ^
                             CicMetaSubst.ppterm_in_context subst hete
                              context ^ " has type " ^
@@ -1027,7 +1043,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 localization_tbl hete msg exn
+                           enrich localization_tbl hete ~f:msg exn
                        | CoercGraph.NotMetaClosed -> 
                            raise (Uncertain (lazy "Coercions on meta"))
                        | CoercGraph.SomeCoercion c ->