diff options
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index f9b73a59eb..a0b0dcf4c8 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -217,7 +217,7 @@ let context_insection sigma ~poly ctx = in let entry = Declare.definition_entry ~univs ~types:t b in let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge - ~kind:Decls.Definition UnivNames.empty_binders entry [] + ~kind:Decls.(IsDefinition Definition) UnivNames.empty_binders entry [] in () in |