The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/31/2014 12:48 PM, Xavier Leroy wrote:
> On 30/07/14 20:11, Jonathan wrote:
> > How about this stop-gap proposal: define an unfold hint db to which users
> > can add their own hints, and which is used by Coq in cases like rewrite and
> > omega (and I'm sure plenty of others).  Or, slightly better - have a setting
> > like "Add Implicit Autounfolds dbname" so that multiple different hint dbs
> > can be used.
> Thanks for the suggestion.  It could work pretty well for my uses in
> CompCert, because I have relatively few type aliases and they get
> reused a lot.  But Coq beginners would still be baffled, first by the
> mysterious failures of rewrite et al, then by the need to build an
> unfold hint db...
>
> Why just a stop-gap and not a proper fix?

What would a proper fix be?  Sometimes, you want rewrite (and other 
tactics) to not do certain conversions.  That means that something is 
needed to distinguish between the conversions you want to be automatic 
and those you don't.

Maybe use Strategy levels somehow?

-- Jonathan