[rewrite foo in hyp] does not work with setoids about math-comp HOT 7 CLOSED

We should move the issue

from math-comp.

Hi Robbert,

This should work using the 'in' tactical, documented in section 6.5 of the manual [https://hal.inria.fr/inria-00258384/en]. Hence changing your

rewrite H1 in H2.
into
rewrite H1 in H2 *.

should work. But there seems to be a bug since H2 is not re-introduced. Hence only
rewrite H1 in H2 * => H2.
works...

from math-comp.

The fact that a 'in H2 *' is needed instead of just 'in H2' is probably due to the internals of setoid rewrite but I cannot yet provide a more informative answer.

from math-comp.

Reporting a comment Georges left on the mailing list:

Here's  what "do [<tactic>] in <hyps>" does:
1) unless there is a *, it replaces the goal with a new manifest constant _the_hidden_goal_
2) it discharges (reverts) Hi in <hyps> using forall/let _discharged_Hi_.
3) it runs <tactic>
4) it introduces the discharged context for each main subgoal derived from the initial goal,
    and undoes 1); nothing is done for side subgoals.

The "tampering" diagnostic indicates step 4) has encountered a goal that has remnants of steps
1) or 2), but no longer has the same shape, which is usually a sign that step 3) has interfered.

from math-comp.

@gares this issue is still current... should we move it to Coq?

from math-comp.

We should move the issue

Looks like that did not happen, but I now reported it on the Coq side: coq/coq#12011

from math-comp.

Closed in favor of coq/coq#12011

from math-comp.