From 00676a80c190c829a85be5545a7cafe16384098f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 1 Apr 2008 08:20:29 +0000
Subject: [PATCH] added set_ppterm

---
 helm/software/components/ng_kernel/nCicPp.ml  | 10 +++++++++-
 helm/software/components/ng_kernel/nCicPp.mli | 12 +++++++++++-
 2 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index a792e865d..6f9a70d50 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -1 +1,9 @@
-let ppterm t = "TODO";;
+let ppterm = 
+  ref (fun ~context ~subst ~metasenv t -> "Please, set a pp callback")
+;;
+
+let set_ppterm f = ppterm := f;;
+
+let ppterm ?(context=[]) ?(subst=[]) ?(metasenv=[]) t = 
+  !ppterm ~context ~subst ~metasenv t
+;;
diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index 3aa3c027d..7a88824c0 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -1 +1,11 @@
-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
-- 
2.39.2