The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hello,

I've got a rewrite database that I use for a lot of simplifications, but a lot of the time that I use it with existentials in the goal it diverges. It's pretty easy to replicate the behavior:

Require Import Plus.

Hint Rewrite <- plus_assoc : test.

Goal exists x, x + 0 = x.

eexists.

do 3 rewrite <- plus_assoc. (** produces a bunch of existentials **)

autorewrite with test. (** diverges **)

Is there any way to tell autorewrite to treat existentials as "atomic," i.e. not be able to expand them arbitrarily? 

Thanks.

--
gregory malecha