removed no longer needed dependency on pxp

[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..f203e6d790edc4b2cc6e413afa8e1c40c6935964 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -62,8 +62,6 @@ type 'a test_result =
 let refine_term metasenv context uri term ugraph =
 (*   if benchmark then incr actual_refinements; *)
   assert (uri=None);
-  let metasenv, term = 
-    CicMkImplicit.expand_implicits metasenv [] context term in
     debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
     try
       let term', _, metasenv',ugraph1 = 
@@ -71,27 +69,26 @@ 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 =
  assert (context = []);
- let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in
    debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
    try
      let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
        (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 +918,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 +938,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