Skip to content

Fix implicit arguments in model/priority/classes.v

Pierre Roux requested to merge proux1/rt-proofs:fix_impl_args into master

Reading proofs about ELF, some hypotheses were neither easy to write nor to read.

It appeared the use of implicit arguments in model/priorities/classes.v was probably a bit too aggressive. Thus, this offers to make some arguments explicits, for the sake of improved clarity.

Note that I only ran through that file, there might be other excessive usages of implicit arguments. In particular, the syntax Context `{TypeClass} seems overused. I'll open a separate PR to warn against that in the guidelines.

Merge request reports