From: Claudio Sacerdoti Coen Date: Mon, 7 Apr 2008 22:04:17 +0000 (+0000) Subject: Pretty-printing of definitions fixed. X-Git-Tag: make_still_working~5413 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d0d82efaff995c566c282af806677bd42d8fd9de;p=helm.git Pretty-printing of definitions fixed. --- diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index b89d44aca..454cc9b58 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -43,12 +43,12 @@ let ppobj = function name ^ " on " ^ string_of_int n ^ " : " ^ ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^ ppterm ~metasenv ~subst ~context:[] bo) fl) - | (u,_,_,_,NCic.Inductive (b, _,tl, _)) -> "inductive" + | (u,_,_,_,NCic.Inductive (b, _,tyl, _)) -> "inductive" | (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 ^ " : " ^ + "definition " ^ name ^ " : " ^ ppterm ~metasenv ~subst ~context:[] ty ^ ":=\n"^ ppterm ~metasenv ~subst ~context:[] bo ^ "\n" ;;