matita/components/ng_extraction/extraction.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: extraction.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
  10
  11 (*s Extraction from Coq terms to Miniml. *)
  12
  13 open Coq
  14 open Miniml
  15 open OcamlExtractionTable
  16
  17 val extract:
  18  #OcamlExtractionTable.status as 'status -> NCic.obj ->
  19   'status * ml_decl list * ml_spec list