Cooking implemented (not tested yet).

[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 ef535cee8f38da02309066c78e465533c2f037d6..96a141ff77e1731fbf52ea33fcea8823f43a56b4 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -5,9 +5,9 @@ val set_ppterm:
     NCic.term -> string) -> unit
 
 val ppterm: 
-  ?context:NCic.context -> 
-  ?subst:NCic.substitution -> 
-  ?metasenv:NCic.metasenv ->
+  context:NCic.context -> 
+  subst:NCic.substitution -> 
+  metasenv:NCic.metasenv ->
    NCic.term -> string
 
 val trivial_pp_term: 
@@ -15,3 +15,5 @@ val trivial_pp_term:
    subst:NCic.substitution -> 
    metasenv:NCic.metasenv ->
     NCic.term -> string
+
+val ppobj: NCic.obj -> string