diff options
| author | Emilio Jesus Gallego Arias | 2020-05-25 14:57:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:10 +0200 |
| commit | a6d663c85d71b3cce007af23419e8030b8c5ac88 (patch) | |
| tree | c610d417d2132edbb2c634d2edf495a4946a0e7e /vernac/comHints.ml | |
| parent | d83e95cce852c5471593a27d0fdca39a262c885f (diff) | |
[declare] [api] Removal of duplicated type aliases.
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 |