type_of_constant was retunrning the type of the wrong constructor (-1 missing)

[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 7a88824c049d8792cce99d2944f2ede4583eff44..ef535cee8f38da02309066c78e465533c2f037d6 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -9,3 +9,9 @@ val ppterm:
   ?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