More information is now printed when reporting errors.

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index fb0666d8dcc0b069e227e79ca845112361c74c68..8f2747a7d6b6de6db5165a380f8bb84d4dbe8131 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -68,13 +68,13 @@ let refine_term metasenv context uri term ugraph =
        CicRefine.type_of_aux' metasenv context term ugraph in
        (Ok (term', metasenv')),ugraph1
     with
-      | CicRefine.Uncertain s ->
-          debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppterm term)) ;
-          Uncertain s,ugraph
+      | CicRefine.Uncertain msg ->
+          debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
+          Uncertain (lazy ("Uncertain trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph
       | CicRefine.RefineFailure msg ->
           debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
             (CicPp.ppterm term) (Lazy.force msg)));
-          Ko msg,ugraph
+          Ko (lazy ("Error trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph
 
 let refine_obj metasenv context uri obj ugraph =
  assert (context = []);
@@ -83,13 +83,13 @@ let refine_obj metasenv context uri obj ugraph =
      let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
        (Ok (obj', metasenv)),ugraph
    with
-     | CicRefine.Uncertain s ->
-         debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppobj obj)) ;
-         Uncertain s,ugraph
+     | CicRefine.Uncertain msg ->
+         debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
+         Uncertain (lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)),ugraph
      | CicRefine.RefineFailure msg ->
          debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
            (CicPp.ppobj obj) (Lazy.force msg))) ;
-         Ko msg,ugraph
+         Ko (lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)),ugraph
 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
   try