* More error messages localized.

[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 5f6c1458ddd7d83f13487e5b8ab13adcb21f0422..9c78c1aa777cba9b7f39b07a4d653ce9c332f9d0 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -309,15 +309,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               match coercion_src with
               | Cic.Sort _ -> 
                   t,type_to_coerce,subst,metasenv,ugraph
-(*
-              | Cic.Meta _ as meta when not in_source -> 
-                  let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
-                  let subst, metasenv, ugraph = 
-                    fo_unif_subst 
-                      subst context metasenv meta coercion_tgt ugraph
-                  in
-                  t, Cic.Sort tgt_sort, subst, metasenv, ugraph
-*)
               | Cic.Meta _ as meta -> 
                   t, meta, subst, metasenv, ugraph
               | Cic.Cast _ as cast -> 
@@ -328,10 +319,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                   let boh = search coercion_src coercion_tgt in
                   (match boh with
                   | CoercGraph.NoCoercion
-                  | CoercGraph.NotHandled _
-                  | CoercGraph.NotMetaClosed -> 
+                  | CoercGraph.NotHandled _ ->
                      enrich localization_tbl t
                       (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
+                  | CoercGraph.NotMetaClosed -> 
+                     enrich localization_tbl t
+                      (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
                   | CoercGraph.SomeCoercion c -> 
                       Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
             in
@@ -372,10 +365,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     | CoercGraph.SomeCoercion c -> 
                        Cic.Appl [c;s'], coercion_tgt
                   | CoercGraph.NoCoercion
-                  | CoercGraph.NotHandled _
-                  | CoercGraph.NotMetaClosed -> 
+                  | CoercGraph.NotHandled _ ->
                      enrich localization_tbl s'
                       (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
+                  | CoercGraph.NotMetaClosed -> 
+                     enrich localization_tbl s'
+                      (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
             in
             let context_for_t = ((Some (n,(C.Decl s')))::context) in 
             let t',type2,subst'',metasenv'',ugraph2 =
@@ -460,9 +455,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                   C.InductiveDefinition (l,expl_params,parsno,_) -> 
                     List.nth l i , expl_params, parsno, u
                 | _ ->
-                    raise
-                      (RefineFailure
-                         (lazy ("Unkown mutual inductive definition " ^ 
+                    enrich localization_tbl t
+                     (RefineFailure
+                       (lazy ("Unkown mutual inductive definition " ^ 
                          U.string_of_uri uri)))
            in
            let rec count_prod t =
@@ -498,8 +493,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
            in
            let actual_type = CicReduction.whd ~subst context actual_type in
            let subst,metasenv,ugraph3 =
+            try
              fo_unif_subst subst context metasenv 
                expected_type' actual_type ugraph2
+            with
+             exn ->
+              enrich localization_tbl term' exn
+               ~f:(function _ ->
+                 lazy ("The term " ^
+                  CicMetaSubst.ppterm_in_context subst term'
+                   context ^ " has type " ^
+                  CicMetaSubst.ppterm_in_context subst actual_type
+                   context ^ " but is here used with type " ^
+                  CicMetaSubst.ppterm_in_context subst expected_type' context))
            in
            let rec instantiate_prod t =
             function
@@ -1032,18 +1038,25 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                        match coer with
                        | CoercGraph.NoCoercion 
                        | CoercGraph.NotHandled _ ->
-                          let msg _e =
-                           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*))
-                          in
-                           enrich localization_tbl hete ~f:msg exn
+                           enrich localization_tbl hete
+                            (RefineFailure
+                              (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*))))
                        | CoercGraph.NotMetaClosed -> 
-                           raise (Uncertain (lazy "Coercions on meta"))
+                           enrich localization_tbl hete
+                            (Uncertain
+                              (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*))))
                        | CoercGraph.SomeCoercion c -> 
                            (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
                    in