NG decompilation is now activated. However, it is called from the old

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 0f835961eeaef5353edd1eafa6110b8ee47e234f..6bcda0df86781d8abe3f61bc5334bed860a2b6e3 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -376,8 +376,7 @@ and try_coercions rdb
       | NCicUnification.Uncertain _ as exc -> first exc tl
   in 
     first exc
-      (NCicCoercion.look_for_coercion 
-        rdb.NRstatus.coerc_db metasenv subst context infty expty)
+      (NCicCoercion.look_for_coercion rdb metasenv subst context infty expty)
 
 and force_to_sort rdb metasenv subst context t orig_t localise ty =
   match NCicReduction.whd ~subst context ty with
@@ -559,7 +558,6 @@ let undebruijnate inductive ref t rev_fl =
 let typeof_obj 
   rdb ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj)
 = 
-prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj));
   let check_type metasenv subst context (ty as orig_ty) =  (* XXX fattorizza *)
     let metasenv, subst, ty, sort = 
       typeof rdb ~localise metasenv subst context ty None