moved the expansion of implicits inside the refiner in a lazy way

[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 7e0996f4f59ef693050b9aef47d03b941c56934a..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 = 
@@ -80,7 +78,6 @@ let refine_term metasenv context uri term 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