diff options
Diffstat (limited to 'contrib/extraction/extraction.mli')
| -rw-r--r-- | contrib/extraction/extraction.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index a44ea2ec0..4c1d492c1 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -4,6 +4,7 @@ open Names open Term open Miniml +open Environ (*s Result of an extraction. *) @@ -18,7 +19,7 @@ type extraction_result = (*s Extraction functions. *) -val extract_constr : constr -> extraction_result +val extract_constr : env -> constr -> extraction_result (*s ML declaration corresponding to a Coq reference. *) |