helm/interface/cicPp.mli

   1 (******************************************************************************)
   2 (*                                                                            *)
   3 (*                               PROJECT HELM                                 *)
   4 (*                                                                            *)
   5 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
   6 (*                                 24/01/2000                                 *)
   7 (*                                                                            *)
   8 (* This module implements a very simple Coq-like pretty printer that, given   *)
   9 (* an object of cic (internal representation) returns a string describing the *)
  10 (* object in a syntax similar to that of coq                                  *)
  11 (*                                                                            *)
  12 (******************************************************************************)
  13
  14 (* ppobj obj  returns a string with describing the cic object obj in a syntax *)
  15 (* similar to the one used by Coq                                             *)
  16 val ppobj : Cic.obj -> string