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 8eff26bae5..dc9c8e2d3c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -204,7 +204,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.(IsDefinition Definition) UnivNames.empty_binders entry [] + ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry in () in |