Initial revision

[helm.git] / helm / interface / cicPp.mli

diff --git a/helm/interface/cicPp.mli b/helm/interface/cicPp.mli
new file mode 100644 (file)
index 0000000..1660799
--- /dev/null
+++ b/helm/interface/cicPp.mli
@@ -0,0 +1,16 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 24/01/2000                                 *)
+(*                                                                            *)
+(* This module implements a very simple Coq-like pretty printer that, given   *)
+(* an object of cic (internal representation) returns a string describing the *)
+(* object in a syntax similar to that of coq                                  *)
+(*                                                                            *)
+(******************************************************************************)
+
+(* ppobj obj  returns a string with describing the cic object obj in a syntax *)
+(* similar to the one used by Coq                                             *)
+val ppobj : Cic.obj -> string