(*s Extraction from Coq terms to Miniml. *)
-open Coq
open Miniml
-open OcamlExtractionTable
val extract:
- #OcamlExtractionTable.status as 'status -> NCic.obj ->
+ (#OcamlExtractionTable.status as 'status) -> NCic.obj ->
'status * ml_decl list * ml_spec list