aboutsummaryrefslogtreecommitdiff
path: root/vernac/comFixpoint.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-02 01:00:56 -0500
committerEmilio Jesus Gallego Arias2020-03-19 17:18:07 -0400
commit069304b4e3ba75c54e372615bf7bb0ee2a103b5d (patch)
tree3b959be77f58ec8c1550310983ff592f9f6fd33c /vernac/comFixpoint.ml
parent9f680f776140c8b3b8f79013262d5bd73761d571 (diff)
[declare] Bring more consistency to parameters using labels
Most of the parameters were named, we fix the remaining cases.
Diffstat (limited to 'vernac/comFixpoint.ml')
-rw-r--r--vernac/comFixpoint.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 8c050b800a..c266178594 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -294,11 +294,11 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
let evd = Evd.from_ctx ctx in
let evd = Evd.restrict_universe_context evd vars in
let ctx = Evd.check_univ_decl ~poly evd pl in
- let udecl = Evd.universe_binders evd in
+ let ubind = Evd.universe_binders evd in
let _ : GlobRef.t list =
- List.map4 (fun name body types imps ->
+ List.map4 (fun name body types impargs ->
let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in
- DeclareDef.declare_definition ~name ~scope ~kind:fix_kind udecl ce imps)
+ DeclareDef.declare_definition ~name ~scope ~kind:fix_kind ~ubind ~impargs ce)
fixnames fixdecls fixtypes fiximps
in
recursive_message (not cofix) gidx fixnames;