diff options
| author | Gaëtan Gilbert | 2020-06-29 10:20:32 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-29 10:20:32 +0200 |
| commit | 61aeca9ca2a7c46b143b90583dfb84b037eccc5b (patch) | |
| tree | 936cab27bacc3bb779aff810be7b79425544f10d /vernac/comHints.ml | |
| parent | 6e5fee168d874b7b6fe7d5c8f4384661bf328d79 (diff) | |
| parent | c62aa0e9d0c33a70822e66a422d4c5926a8c8df7 (diff) | |
Merge PR #12372: [declare] Refactor constant information into a record.
Reviewed-by: SkySkimmer
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 |