The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Vadim,

It's more likely to be failing unifications that take a long time indeed. It's easy to check which it is using Set Typeclasses Depth 0 which will make resolution fail immediately. Maybe using Hint Opaque foo : rewrite. for a few constants you don't want to unfold during unification of the lemma would help (these hints are used by setoid_rewrite).

Hope this helps,

-- Matthieu

Le jeu. 18 août 2016 à 01:56, Vadim Zaliva <vzaliva AT cmu.edu> a écrit :

On Wed, Aug 17, 2016 at 4:16 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

expressions 'a' and 'b' are approximately 400 lines long each. Even if I use (set with wildcards trick proposed by Laurent, I do not have to spell out 'a' but I still need manually construct and write down 'b'. So making 'setoid_rewrite ... at n' could really help here.

Found another workaround which allows to avoid spelling full expressions:

  remember (compose (foo _ ) _) as c1 eqn: Hc1.

  setoid_rewrite <- compose_assoc in Hc1.

  subst c1.

but it is still hacky...

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060