- fixed hint generation, more hints are generated

[helm.git] / helm / software / components / ng_kernel / nCicPp.ml

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 59d6bcf488ba98bcabcf39f6fdf7b766f9b2928c..42b05d10e46561265b1186b292c333e9ca3d408d 100644 (file)
--- 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 "(";