better print of ILLEGAL applications

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index e7cc53a47b8de4030032bd1858afdf63c08584e5..006a8a7a5f4fec44529d2e623c7852ea0a6858f4 100644 (file)
--- 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