ocaml 3.09 transition

[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 681ed492979851c963abbbf27ad9b3f181008a10..d3a297d43e88b517cec0e9caf4eef32e322896d9 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
@@ -392,12 +398,13 @@ and type_of_aux' metasenv context t ugraph =
                   let search = CoercGraph.look_for_coercion in
                   let boh = search coercion_src coercion_tgt in
                   (match boh with
-                  | CoercGraph.NoCoercion ->
-                      raise (RefineFailure (lazy "no coercion"))
+                  | CoercGraph.NoCoercion
                   | CoercGraph.NotHandled _ -> 
-                      raise (RefineFailure (lazy "not a sort in PI"))
+                     raise
+                      (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
                   | CoercGraph.NotMetaClosed -> 
-                      raise (Uncertain (lazy "Coercions on metas 1"))
+                     raise
+                      (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)
             in
@@ -483,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"))
@@ -1100,7 +1115,17 @@ and type_of_aux' metasenv context t ugraph =
                        in
                        match coer with
                        | CoercGraph.NoCoercion 
-                       | CoercGraph.NotHandled _ -> raise exn
+                       | 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 msg exn
                        | CoercGraph.NotMetaClosed -> 
                            raise (Uncertain (lazy "Coercions on meta"))
                        | CoercGraph.SomeCoercion c ->