]> matita.cs.unibo.it Git - helm.git/commitdiff
better print of ILLEGAL applications
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 1 Sep 2009 17:11:41 +0000 (17:11 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 1 Sep 2009 17:11:41 +0000 (17:11 +0000)
helm/software/components/ng_kernel/nCicPp.ml

index e7cc53a47b8de4030032bd1858afdf63c08584e5..006a8a7a5f4fec44529d2e623c7852ea0a6858f4 100644 (file)
@@ -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