aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comAssumption.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comAssumption.mli')
-rw-r--r--vernac/comAssumption.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 2f2c7c4e2..56932360a 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -30,6 +30,6 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
nor in a module type and meant to be instantiated. *)
val declare_assumption : coercion_flag -> assumption_kind ->
types in_constant_universes_entry ->
- Universes.universe_binders -> Impargs.manual_implicits ->
+ UnivNames.universe_binders -> Impargs.manual_implicits ->
bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
GlobRef.t * Univ.Instance.t * bool