]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicPp.mli
Initial implementation of statuses using objects in place of nested records.
[helm.git] / helm / software / components / ng_kernel / nCicPp.mli
index e8b7c6dab465f6c4c6107d4b7050de7607661471..c260e8c61a70c9f1c29f80e9b0f3c6367bb10eea 100644 (file)
@@ -12,6 +12,9 @@
 (* $Id$ *)
 
 val set_head_beta_reduce: (upto:int -> NCic.term -> NCic.term) -> unit
+val set_get_obj: (NUri.uri -> NCic.obj) -> unit
+
+val r2s: bool -> NReference.reference -> string
 
 val ppterm: 
   context:NCic.context ->