]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/cicPp.mli
Requires and Provides now fixed
[helm.git] / 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