1 (************************************************************************)
2 (* v * The Coq Proof Assistant / The Coq Development Team *)
3 (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
4 (* \VV/ **************************************************************)
5 (* // * This file is distributed under the terms of the *)
6 (* * GNU Lesser General Public License Version 2.1 *)
7 (************************************************************************)
9 (*i $Id: ocaml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
13 open OcamlExtractionTable
15 val pp_decl : #status as 'status -> ml_decl -> 'status * std_ppcmds
16 val pp_spec : #status as 'status -> ml_spec -> 'status * std_ppcmds
17 val pp_open : #status as 'status -> string -> 'status * std_ppcmds