From: Enrico Tassi Date: Mon, 28 Sep 2009 14:38:13 +0000 (+0000) Subject: better debug pp X-Git-Tag: make_still_working~3428 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3a4c39fc9c938ca155f0e807525cd38eec240a0d;p=helm.git better debug pp --- diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index ce109f2af..3d89161b3 100644 --- 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