Less verbose error messages.

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index f8fa77dc67b894f6bc5a77f2a820ac65942f2f75..8bdb409e923ed19387be8a66fb1b765492ceb582 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -70,11 +70,11 @@ let refine_term metasenv context uri term ugraph =
     with
       | CicRefine.Uncertain msg ->
           debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
-          Uncertain (lazy ("Uncertain trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)),ugraph
+          Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph
       | CicRefine.RefineFailure msg ->
           debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
             (CicPp.ppterm term) (Lazy.force msg)));
-          Ko (lazy ("Error trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)),ugraph
+          Ko (msg (*lazy ("Error trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph
 
 let refine_obj metasenv context uri obj ugraph =
  assert (context = []);
@@ -85,11 +85,11 @@ let refine_obj metasenv context uri obj ugraph =
    with
      | 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
+         Uncertain (msg (*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 (lazy ("Error trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)),ugraph
+         Ko (msg (*lazy ("Error trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph
 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
   try