aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/extract_env.ml1
-rw-r--r--contrib/extraction/haskell.mli2
2 files changed, 2 insertions, 1 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 93e8d4cf50..68ff965b25 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -10,6 +10,7 @@
open Pp
open Util
+open Names
open Term
open Lib
open Extraction
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 77bea2b8b5..4f380271f5 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -12,7 +12,7 @@
open Miniml
open Mlutil
-open Term
+open Names
val extract_to_file :
string -> extraction_params -> ml_decl list -> global_reference list -> unit