diff options
Diffstat (limited to 'plugins/extraction/extraction.mli')
| -rw-r--r-- | plugins/extraction/extraction.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 1eb9ca8e5..3a5fc9794 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -19,7 +19,7 @@ val extract_constant : env -> constant -> constant_body -> ml_decl val extract_constant_spec : env -> constant -> constant_body -> ml_spec -val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) option +val extract_with_type : env -> constant_body -> ( Id.t list * ml_type ) option val extract_fixpoint : env -> constant array -> (constr, types) prec_declaration -> ml_decl |