better error message

[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 96a141ff77e1731fbf52ea33fcea8823f43a56b4..5a7fd75a9d27f148e558467fa85965aff8b025c8 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -2,18 +2,21 @@ 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 trivial_pp_term: 
    context:NCic.context -> 
    subst:NCic.substitution -> 
    metasenv:NCic.metasenv ->
+   ?inside_fix:bool ->
     NCic.term -> string
 
 val ppobj: NCic.obj -> string