Skip to content

Revise uses of `inj` from !408 as discussed

Paolo G. Giarrusso requested to merge Blaisorblade/iris:inj-typeclass-2 into master

Also fix one use of inj _ from before !408 (merged). There's one leftover from sum_ofe_mixin, but I'd leave it alone tho it's pretty weird:

$ git grep '\binj\b _'
theories/algebra/ofe.v:      + destruct (Hx 0); constructor; apply equiv_dist=> n; by apply (inj _).

because this would be the fix:

-      + destruct (Hx 0); constructor; apply equiv_dist=> n; by apply (inj _).
+      + destruct (Hx 0); constructor; apply equiv_dist=> n; by [apply (inj inl)|apply (inj inr)].
Edited by Paolo G. Giarrusso

Merge request reports