From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 19 Dec 2008 10:11:39 +0000 (+0000)
Subject: handles bad Appl
X-Git-Tag: make_still_working~4358
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b91dfc5e2b00e6b0b4cb81109192bb2b825055a1;p=helm.git

handles bad Appl
---

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 59d6bcf48..42b05d10e 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -126,6 +126,8 @@ let ppterm ~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 l -> 
        F.fprintf f "@[<hov 2>";
        if not toplevel then F.fprintf f "(";