diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 67733c95a1..f044c025d8 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -54,7 +54,7 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = | Global local -> let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in let gr = Names.GlobRef.ConstRef kn in - let () = Declare.declare_univ_binders gr udecl in + let () = DeclareUniv.declare_univ_binders gr udecl in gr in let () = maybe_declare_manual_implicits false gr imps in |