aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/classes.ml')
-rw-r--r--vernac/classes.ml10
1 files changed, 5 insertions, 5 deletions
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