Adapt to coq/coq#13837 ("apply with" does not rename arguments)

uwplse / verdi-raft

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

BSD 2-Clause "Simplified" License

182 stars 19 forks source link

Adapt to coq/coq#13837 ("apply with" does not rename arguments) #88

Closed SkySkimmer closed 2 years ago

SkySkimmer commented 2 years ago

Should be backwards compatible.

(part2)

Note the strange rewrite <- deghost_spec with (net0 := net). to rename net into net0; rewrite <- deghost_spec with (net := net0). changes: here the usual @ patch does not work because rewrite does some black magic dependent on implicit arguments. When we drop backwards compat we can just do the saner rewrite <- deghost_spec with (net := net).

SkySkimmer commented 2 years ago

I didn't finish compiling before submitting the previous PR so it was incomplete, this one is complete though.