aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comAssumption.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comAssumption.mli')
-rw-r--r--vernac/comAssumption.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index a2d20a1d1..2f2c7c4e2 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -11,7 +11,6 @@
open Names
open Constr
open Entries
-open Globnames
open Vernacexpr
open Constrexpr
open Decl_kinds
@@ -33,4 +32,4 @@ val declare_assumption : coercion_flag -> assumption_kind ->
types in_constant_universes_entry ->
Universes.universe_binders -> Impargs.manual_implicits ->
bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
- global_reference * Univ.Instance.t * bool
+ GlobRef.t * Univ.Instance.t * bool