branch for universe

[helm.git] / components / ng_kernel / nCicPp.mli

diff --git a/components/ng_kernel/nCicPp.mli b/components/ng_kernel/nCicPp.mli
new file mode 100644 (file)
index 0000000..1dbdead
--- /dev/null
+++ b/components/ng_kernel/nCicPp.mli
@@ -0,0 +1,27 @@
+val set_ppterm: 
+  (context:NCic.context -> 
+   subst:NCic.substitution -> 
+   metasenv:NCic.metasenv ->
+   ?inside_fix:bool ->
+    NCic.term -> string) -> unit
+
+val ppterm: 
+  context:NCic.context -> 
+  subst:NCic.substitution -> 
+  metasenv:NCic.metasenv ->
+  ?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 -> 
+   metasenv:NCic.metasenv ->
+   ?inside_fix:bool ->
+    NCic.term -> string
+
+val ppobj: NCic.obj -> string