From b49c4ade22239e671012537d598e7b2bc17c419e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Apr 2008 14:59:43 +0000 Subject: [PATCH 1/1] added case of const and axiom --- helm/software/components/ng_kernel/nCicPp.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 94acaf3f4..b89d44aca 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -44,7 +44,13 @@ let ppobj = function ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^ ppterm ~metasenv ~subst ~context:[] bo) fl) | (u,_,_,_,NCic.Inductive (b, _,tl, _)) -> "inductive" - | (u,_,_,_,NCic.Constant (_,_,_, _, _)) -> "constant" + | (u,_,metasenv,subst,NCic.Constant (_,name,None,ty, _)) -> + "axiom " ^ name ^ " : " ^ + ppterm ~metasenv ~subst ~context:[] ty ^ "\n" + | (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) -> + "axiom " ^ name ^ " : " ^ + ppterm ~metasenv ~subst ~context:[] ty ^ ":=\n"^ + ppterm ~metasenv ~subst ~context:[] bo ^ "\n" ;; -- 2.39.2