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 2fa156abd..0491638c9 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -30,5 +30,5 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
val declare_assumption : coercion_flag -> assumption_kind ->
types in_constant_universes_entry ->
Universes.universe_binders -> Impargs.manual_implicits ->
- bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
+ bool (** implicit *) -> Vernacexpr.inline -> variable CAst.t ->
global_reference * Univ.Instance.t * bool