Christian Doczkal

> @chdoc cf [coq/coq#12780](https://github.com/coq/coq/issues/12780) Yes, I had seen that issue, and I agree that it is probably related. However, since in this instance `rewrite -> ifN` succeeds while `rewrite ifN`...

Now that CI has finished, it appears that the only development using `closed` and/or `closure` is indeed `fourcolor`. I haven't looked at this yet, but I expect that in fourcolor...

So you knew and choose not to do anything about it?

Well, why have `ltn_addr` in the first place, this is just an instance of the long form of `leq_addr` with `m := m.+1`

So what's the course of action, if any? Remove/deprecate `ltn_addr` in favor of a long form for `leq_addr`? How should this long form be named?

I would be happy to have a bare-bones implementation that I can play around with sooner rather than later. Unfortunately, I'm not very good at elisp. But now that you...

> And we should also decide which keybinding would be OK for the three steps involved In my setup (PG + company-coq) `C-c r` is unbound. How about: - `C-c...

> I think this feature goes beyong ssreflect. I have been thinking about something like this for the `;` tactical. Debuging `foo;bar;rab;oof` boils down to the same mechanics really. You...

> As a "concrete" syntax I would propose an attribute `#[expand]` that is ignored by "lines" for which the system does not know how to compute an expansion, while it...

Well, I would be happy with a prototype that handles only the `[by] rewrite` from ssreflect. The reason for this is that there is a plan to remove occurrence selectors...