X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=cf44ff4708946917e62fd397479caea6af471365;hb=1409a972815b8e4e697d9ad55c77d9292cbea787;hp=ce109f2af906353375c4504c07eea230a4de5611;hpb=849c15ec9cc74737cbf5d392fa565e0630f903d7;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index ce109f2af..cf44ff470 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -15,11 +15,6 @@ exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
-let refiner_typeof =
- ref (fun _ ?localise _ _ _ _ _ -> ignore localise; assert false);;
-let set_refiner_typeof f = refiner_typeof := f
-;;
-
 let (===) x y = Pervasives.compare x y = 0 ;;
 
 let uncert_exc metasenv subst context t1 t2 = 
@@ -222,6 +217,10 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
               assert false)
          | NCicTypeChecker.TypeCheckerFailure msg ->
               prerr_endline (Lazy.force msg);
+       prerr_endline (
+               "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
+          ppcontext ~metasenv ~subst context ^ 
+          ppmetasenv ~subst metasenv);
               pp msg; assert false
        in
        let lty = NCicSubstitution.subst_meta lc ty in