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