More errors 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 35c92a4139210085c47084ca153e73851c20b703..5f6c1458ddd7d83f13487e5b8ab13adcb21f0422 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -291,30 +291,30 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
               with
                exn ->
-                enrich localization_tbl t
+                enrich localization_tbl te'
                  ~f:(fun _ ->
                    lazy ("The term " ^
-                    CicMetaSubst.ppterm_in_context subst'' te
+                    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
+                    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 
-              in_source tgt_sort t type_to_coerce subst ctx metasenv uragph 
+            let coerce_to_sort in_source tgt_sort t type_to_coerce
+                 subst context metasenv uragph 
             =
-              let coercion_src = carr type_to_coerce subst ctx in
+              let coercion_src = carr type_to_coerce subst context in
               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 ctx in
+                  let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
                   let subst, metasenv, ugraph = 
                     fo_unif_subst 
-                      subst ctx metasenv meta coercion_tgt ugraph
+                      subst context metasenv meta coercion_tgt ugraph
                   in
                   t, Cic.Sort tgt_sort, subst, metasenv, ugraph
 *)
@@ -323,17 +323,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               | Cic.Cast _ as cast -> 
                   t, cast, subst, metasenv, ugraph
               | term -> 
-                  let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
+                  let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
                   let search = CoercGraph.look_for_coercion in
                   let boh = search coercion_src coercion_tgt in
                   (match boh with
                   | CoercGraph.NoCoercion
-                  | CoercGraph.NotHandled _ -> 
-                     enrich localization_tbl s
-                      (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
+                  | CoercGraph.NotHandled _
                   | CoercGraph.NotMetaClosed -> 
-                     enrich localization_tbl s
-                      (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
+                     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.SomeCoercion c -> 
                       Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
             in
@@ -376,8 +374,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                   | CoercGraph.NoCoercion
                   | CoercGraph.NotHandled _
                   | CoercGraph.NotMetaClosed -> 
-                     raise (RefineFailure (lazy (sprintf
-                      "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))))
+                     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")))
             in
             let context_for_t = ((Some (n,(C.Decl s')))::context) in 
             let t',type2,subst'',metasenv'',ugraph2 =
@@ -420,7 +418,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 hetype tlbody_and_type ugraph2
             in
               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
-        | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
+        | C.Appl _ -> assert false
         | C.Const (uri,exp_named_subst) ->
             let exp_named_subst',subst',metasenv',ugraph1 =
               check_exp_named_subst subst metasenv context