From 4940f99922b0784d726b7c50abe63395713f012f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 17 Nov 2017 23:48:21 +0100
Subject: Fix #5347: unify declaration of axioms with and without bound univs.

Note that this makes the following syntax valid:

     Axiom foo@{i} bar : Type@{i}.

(ie putting a universe declaration on the first axiom in the list, the
declaration then holds for the whole list).
---
 vernac/command.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/command.mli')

diff --git a/vernac/command.mli b/vernac/command.mli
index fb99a717b9..070f3e1120 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -43,7 +43,7 @@ val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr opt
 (** returns [false] if the assumption is neither local to a section,
     nor in a module type and meant to be instantiated. *)
 val declare_assumption : coercion_flag -> assumption_kind -> 
-  types Univ.in_universe_context_set ->
+  types in_constant_universes_entry ->
   Universes.universe_binders -> Impargs.manual_implicits ->
   bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
   global_reference * Univ.Instance.t * bool
-- 
cgit v1.2.3