added ppcontext

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 782fd9566ba53f5af38a7825b31eec1d7bd10262..72088e48b1c4bd9b1544ce228c0590ded9056464 100644 (file)
--- 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 5a7fd75a9d27f148e558467fa85965aff8b025c8..1dbdeadc0155df1a08c4eb71a919755e55a94ecc 100644 (file)
--- 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 ->