From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 22 Apr 2008 12:47:31 +0000 (+0000)
Subject: added ppcontext
X-Git-Tag: make_still_working~5301
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d33b08df0d8929dff96f4c7499cd819103d2bb5c;p=helm.git

added ppcontext
---

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 ->