diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 01:00:56 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:07 -0400 |
| commit | 069304b4e3ba75c54e372615bf7bb0ee2a103b5d (patch) | |
| tree | 3b959be77f58ec8c1550310983ff592f9f6fd33c /vernac/comAssumption.ml | |
| parent | 9f680f776140c8b3b8f79013262d5bd73761d571 (diff) | |
[declare] Bring more consistency to parameters using labels
Most of the parameters were named, we fix the remaining cases.
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 |