some debug printings

[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 7af5d17a6f6e1e7a950184575784601ca0a700c6..b21274fea109915daca66ea3d1aab10f3501b9d2 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -42,7 +42,8 @@ let ppobj = function
         (List.map (fun (_,name,n,ty,bo) ->
           name ^ " on " ^ string_of_int n ^ " : " ^ ppterm ty ^ " :=\n"^
           ppterm bo) fl)
-  | _ -> "todo"
+  | (u,_,_,_,NCic.Inductive (b, _,tl, _)) -> "inductive"
+  | (u,_,_,_,NCic.Constant (_,_,_, _, _)) -> "constant"
 ;;