Every exception that used to have type string is now a string Lazy.t.

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 51c124a9b5d83824d0f5ba128460d2bc0ef49e6c..7e0996f4f59ef693050b9aef47d03b941c56934a 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -71,11 +71,11 @@ let refine_term metasenv context uri term ugraph =
        (Ok (term', metasenv')),ugraph1
     with
       | CicRefine.Uncertain s ->
-          debug_print (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term)) ;
+          debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppterm term)) ;
           Uncertain,ugraph
       | CicRefine.RefineFailure msg ->
           debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
-            (CicPp.ppterm term) (CicRefine.explain_error msg)));
+            (CicPp.ppterm term) (Lazy.force msg)));
           Ko,ugraph
 
 let refine_obj metasenv context uri obj ugraph =
@@ -87,11 +87,11 @@ let refine_obj metasenv context uri obj ugraph =
        (Ok (obj', metasenv)),ugraph
    with
      | CicRefine.Uncertain s ->
-         debug_print (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj)) ;
+         debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppobj obj)) ;
          Uncertain,ugraph
      | CicRefine.RefineFailure msg ->
          debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
-           (CicPp.ppobj obj) (CicRefine.explain_error msg))) ;
+           (CicPp.ppobj obj) (Lazy.force msg))) ;
          Ko,ugraph
 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
@@ -921,7 +921,7 @@ in refine_profiler.HExtlib.profile foo ()
 
 module Trivial =
 struct
-  exception Ambiguous_term of string
+  exception Ambiguous_term of string Lazy.t
   exception Exit
   module Callbacks =
   struct
@@ -941,6 +941,6 @@ struct
     try
       fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
         ?initial_ugraph ~aliases ~universe:None)
-    with Exit -> raise (Ambiguous_term term)
+    with Exit -> raise (Ambiguous_term (lazy term))
 end