Anton Trunov

Did this ever happen? I'd absolutely love to have this feature!

And if it didn't happen yet, is there a workaround?

Looks like this is a related issue: https://github.com/smtcoq/sniper/issues/4

This would be great to have! It's kind of a blocker for a project I'm working on to support Coq 8.15.

Interesting. I know at least one place in the standard library where the proof relies on this simplification: [here](https://github.com/coq/coq/blob/2d6e395dead61a49ede6208bc40e16b4b8e68ce4/theories/Numbers/Cyclic/Int31/Cyclic31.v#L1732) (`(31 - size)` simplifies to zero).

FWIW, I switched to [Spacemacs](https://github.com/syl20bnr/spacemacs) because of this issue. Nowadays, I bind `,.` to `proof-goto-point` in normal mode.

I think this issue should be moved to Coq's GitHub. Here are two more workarounds: 1. Make all the following arguments of `in_app_or` maximally-inserted implicit: ```coq Arguments in_app_or {A l...

@CohenCyril @gares I think either of you can move the issue to Coq with this GitHub feature -- https://help.github.com/articles/transferring-an-issue-to-another-repository/

I guess one needs to be a member of both organizations (from/to) to do that. I thought it was the case.

Somehow I missed that part. Sorry for the false alarm.