matita/components/ng_extraction/ocaml.mli

   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 (************************************************************************)
   8
   9 (*i $Id: ocaml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
  10
  11 open Coq
  12 open Miniml
  13 open OcamlExtractionTable
  14
  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