]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/cicPp.mli
This commit was manufactured by cvs2svn to create branch 'helm'.
[helm.git] / helm / interface / cicPp.mli
diff --git a/helm/interface/cicPp.mli b/helm/interface/cicPp.mli
deleted file mode 100644 (file)
index 1660799..0000000
+++ /dev/null
@@ -1,16 +0,0 @@
-(******************************************************************************)
-(*                                                                            *)
-(*                               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