summaryrefslogtreecommitdiff
path: root/plugins/extraction/common.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/common.mli')
-rw-r--r--plugins/extraction/common.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 78545c8b..07237d75 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Globnames
open Miniml
(** By default, in module Format, you can do horizontal placing of blocks
@@ -54,7 +53,7 @@ val opened_libraries : unit -> ModPath.t list
type kind = Term | Type | Cons | Mod
-val pp_global : kind -> global_reference -> string
+val pp_global : kind -> GlobRef.t -> string
val pp_module : ModPath.t -> string
val top_visible_mp : unit -> ModPath.t