From d0d82efaff995c566c282af806677bd42d8fd9de Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 7 Apr 2008 22:04:17 +0000 Subject: [PATCH] Pretty-printing of definitions fixed. --- helm/software/components/ng_kernel/nCicPp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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" ;; -- 2.39.2