- fixed hint generation, more hints are generated

[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 50204fe990d08ed057e4011182ef0fc41a277058..507f38d162ded2b801ea873939d3f6bbde82f504 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -11,13 +11,6 @@
 
 (* $Id$ *)
 
-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 -> 
@@ -26,15 +19,14 @@ val ppterm:
    NCic.term -> string
 
 val ppcontext:
+  ?sep:string ->
   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 ppmetasenv:
+  subst:NCic.substitution -> NCic.metasenv -> string
+
+val ppsubst: metasenv:NCic.metasenv -> NCic.substitution -> string
 
 val ppobj: NCic.obj -> string