X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=f203e6d790edc4b2cc6e413afa8e1c40c6935964;hb=4f00a766afd24d51314badcab74cea2ccf623e28;hp=7e0996f4f59ef693050b9aef47d03b941c56934a;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 7e0996f4f..f203e6d79 100644
--- 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