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/classes.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 1833b7a1d..b80741269 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -412,15 +412,15 @@ let context poly l = in let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) + else Monomorphic_const_entry !uctx + in let nstatus = match b with | None -> - pi3 (Command.declare_assumption false decl (t, !uctx) Universes.empty_binders [] impl + pi3 (Command.declare_assumption false decl (t, univs) Universes.empty_binders [] impl Vernacexpr.NoInline (Loc.tag id)) | Some b -> - let univs = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) - else Monomorphic_const_entry !uctx - in let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in -- cgit v1.2.3