From d33b08df0d8929dff96f4c7499cd819103d2bb5c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 22 Apr 2008 12:47:31 +0000 Subject: [PATCH] added ppcontext --- helm/software/components/ng_kernel/nCicPp.ml | 11 +++++++++++ helm/software/components/ng_kernel/nCicPp.mli | 5 +++++ 2 files changed, 16 insertions(+) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 782fd9566..72088e48b 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -160,3 +160,14 @@ let ppobj = function ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^ ppterm ~metasenv ~subst ~context:[] bo ^ "\n" ;; + +let rec ppcontext ~subst ~metasenv = function + | [] -> "" + | (name, NCic.Decl t) :: tl -> + ppcontext ~subst ~metasenv tl ^ + name ^ ": " ^ ppterm ~subst ~metasenv ~context:tl t ^ "\n" + | (name, NCic.Def (bo,ty)) :: tl-> + ppcontext ~subst ~metasenv tl ^ + name ^ ": " ^ ppterm ~subst ~metasenv ~context:tl ty ^ + " := " ^ ppterm ~subst ~metasenv ~context:tl bo ^ "\n" +;; diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli index 5a7fd75a9..1dbdeadc0 100644 --- a/helm/software/components/ng_kernel/nCicPp.mli +++ b/helm/software/components/ng_kernel/nCicPp.mli @@ -12,6 +12,11 @@ val ppterm: ?inside_fix:bool -> NCic.term -> string +val ppcontext: + subst:NCic.substitution -> + metasenv:NCic.metasenv -> + NCic.context -> string + val trivial_pp_term: context:NCic.context -> subst:NCic.substitution -> -- 2.39.2