blob: 3e6c9c275f67d3b9905c948fe93a3f41d37918e5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(*i $Id$ i*)
open Names
open Term
open Miniml
(*s Result of an extraction. *)
type type_var = Varity | Vskip
type signature = (type_var * identifier) list
type extraction_result =
| Emltype of ml_type * signature * identifier list
| Emlterm of ml_ast
(*s Extraction functions. *)
val extract_constr : constr -> extraction_result
(*s ML declaration corresponding to a Coq reference. *)
val extract_declaration : global_reference -> ml_decl
|
