better debug pp

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

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index ce109f2af906353375c4504c07eea230a4de5611..3d89161b3220a770e69582e09da11271267377f5 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -222,6 +222,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