"Localization" of error messages for eat_prods and applications.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 21bf072781c43cbfd3595090fe41f282e01febd2..202fa8cd798d3495a544f581128f2d510303c231 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -42,6 +42,12 @@ in profiler.HExtlib.profile foo ()
       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
 ;;
+
+let enrich f =
+ function
+    RefineFailure msg -> raise (RefineFailure (f msg))
+  | Uncertain msg -> raise (Uncertain (f msg))
+  | _ -> assert false
                        
 let rec split l n =
  match (l,n) with
@@ -484,8 +490,16 @@ and type_of_aux' metasenv context t ugraph =
                 ) tl ([],subst',metasenv',ugraph1)
             in
             let tl',applty,subst''',metasenv''',ugraph3 =
+             try
               eat_prods true subst'' metasenv'' context 
                 hetype tlbody_and_type ugraph2
+             with
+              exn ->
+               enrich
+                (fun msg ->
+                  lazy ("The application " ^
+                   CicMetaSubst.ppterm_in_context subst'' t context ^
+                  " is not well typed:\n" ^ Lazy.force msg)) exn
             in
               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
         | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
@@ -1101,7 +1115,16 @@ and type_of_aux' metasenv context t ugraph =
                        in
                        match coer with
                        | CoercGraph.NoCoercion 
-                       | CoercGraph.NotHandled _ -> raise exn
+                       | CoercGraph.NotHandled _ ->
+                          let msg =
+                           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)
+                          in
+                           enrich (fun _ -> msg) exn
                        | CoercGraph.NotMetaClosed -> 
                            raise (Uncertain (lazy "Coercions on meta"))
                        | CoercGraph.SomeCoercion c ->