From 72a3999ca5a4a2168753c272063ea6530dc963bd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Sep 2009 17:11:41 +0000 Subject: [PATCH] better print of ILLEGAL applications --- helm/software/components/ng_kernel/nCicPp.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index e7cc53a47..006a8a7a5 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -135,8 +135,14 @@ let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t = 2 (List.tl pl)); end; F.fprintf f "]@] @]"; - | C.Appl [] | C.Appl [_] | C.Appl (C.Appl _::_) -> - F.fprintf f "BAD APPLICATION" + | C.Appl [] -> + F.fprintf f "BAD APPLICATION: empty list" + | C.Appl [x] -> + F.fprintf f "BAD APPLICATION: just the head: "; + aux ctx x + | C.Appl (C.Appl _ as x::_) -> + F.fprintf f "BAD APPLICATION: appl of appl with head: "; + aux ctx x | C.Appl (C.Meta (n,lc) :: args) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in let hd = NCicSubstitution.subst_meta lc t in -- 2.39.2