]> matita.cs.unibo.it Git - helm.git/commitdiff
better debug pp
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 28 Sep 2009 14:38:13 +0000 (14:38 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 28 Sep 2009 14:38:13 +0000 (14:38 +0000)
helm/software/components/ng_refiner/nCicUnification.ml

index ce109f2af906353375c4504c07eea230a4de5611..3d89161b3220a770e69582e09da11271267377f5 100644 (file)
@@ -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