diff options
Diffstat (limited to 'vernac/comHints.ml')
| -rw-r--r-- | vernac/comHints.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comHints.ml b/vernac/comHints.ml index ec37ec7fa8..b05bf9a675 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -56,7 +56,7 @@ let project_hint ~poly pri l2r r = Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c)) in let c = - Declare.declare_constant ~local:Declare.ImportDefaultBehavior ~name + Declare.declare_constant ~local:Locality.ImportDefaultBehavior ~name ~kind:Decls.(IsDefinition Definition) cb in |