From 3a4c39fc9c938ca155f0e807525cd38eec240a0d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 28 Sep 2009 14:38:13 +0000 Subject: [PATCH] better debug pp --- helm/software/components/ng_refiner/nCicUnification.ml | 4 ++++ 1 file changed, 4 insertions(+) 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 -- 2.39.2