The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Is anyone else experiencing extremely slow "rewrite in *|-" in recent 8.5?

I compared a problematic rewrite in *|- against a 
repeat/match/context/rewrite tactic that does the same set of rewrites 
in the goal, and the rewrite in *|- was 8X slower.  But, removing the 
context pattern removes the 8X speedup.

Schematically, I did this:

  Lemma RW : forall ... L = R.

  ...

  Time rewrite ?RW in *|-.  (*takes 2.6 secs*)
  Undo.
  Time repeat match goal with
             | H : context [L] |- _ => rewrite RW in H  end. (*takes 
0.3 secs*)
  Undo.
  Time repeat match goal with
             | H : _ |- _ => rewrite RW in H end. (*takes 2.3 secs*)

So, in other words, the context pattern speeds things up 8X.

This is in 8.5 beta3, git version 951b332.  I don't know if this speed 
anomaly existed prior to 8.5beta3 - but I can try earlier versions, if 
someone suggests one to try.

-- Jonathan