I often meet proofs using
autorewrite which Coq takes a while to process for some reason. (Setoid rewriting)
I then manually figure out which rewrite rules were applied and perform the steps manually or semi-automatically. Often applying
Proper by hand is quicker.
Is there some way to have Coq tell me which rules
autorewrite applied? Possibly also how it instantiated the variables.
I found issue #9285, but it does not mention existing features.
Edit: Link to the relevant page of the reference manual on Programmable Proof Search
autorewrite tactic is described.