* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* 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 *)
-(* *)
-(******************************************************************************)
+(*****************************************************************************)
+(* *)
+(* 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 *)
+(* 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
val ppterm : Cic.term -> string
+val ppcontext : ?sep:string -> Cic.context -> string
+
(* Required only by the topLevel. It is the generalization of ppterm to *)
(* work with environments. *)
val pp : Cic.term -> (Cic.name option) list -> string
+
+val ppname : Cic.name -> string
+