diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index ba4b42c4e0..bd857a6e38 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -87,6 +87,8 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = let kn = Declare.declare_constant ~name ~local ~kind decl in let dref = Names.GlobRef.ConstRef kn in let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = Declare.assumption_message name in + let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in dref |