context, metasenv and subst made mandatory in CicPp

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

diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index 3aa3c027d34d3f91b7876cf90cea0aa0905b0b64..96a141ff77e1731fbf52ea33fcea8823f43a56b4 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -1 +1,19 @@
-val ppterm: NCic.term -> string
+val set_ppterm: 
+  (context:NCic.context -> 
+   subst:NCic.substitution -> 
+   metasenv:NCic.metasenv ->
+    NCic.term -> string) -> unit
+
+val ppterm: 
+  context:NCic.context -> 
+  subst:NCic.substitution -> 
+  metasenv:NCic.metasenv ->
+   NCic.term -> string
+
+val trivial_pp_term: 
+   context:NCic.context -> 
+   subst:NCic.substitution -> 
+   metasenv:NCic.metasenv ->
+    NCic.term -> string
+
+val ppobj: NCic.obj -> string