The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/31/2014 01:33 PM, Jason Gross wrote:
> Would something like the feature request I made for more opacity levels
> <https://coq.inria.fr/bugs/show_bug.cgi?id=3389> fix this problem?
>
> -Jason

It would certainly make some things easier.  Although I don't fully 
understand what distinguishes all those new levels, I can see that some 
(like expand_invisible) would be helpful.

But, although I brought up Strategy levels, I did so somewhat 
half-heartedly.  They seem very ad-hoc, the kind of thing that one 
doesn't mind so much in syntax (as with Notation levels), but wonders 
about maybe causing problems in semantics.  Giving names to levels helps 
vs. just numbers, though - but maybe not enough.

I also want to make a comment about decision procedures like omega and 
lia: I think it is hard to see cases for decision procedures where 
preventing conversion (at least when allowing it wouldn't cause 
termination or severe performance problems) is a good thing. But, 
consider a tactic like ring_simplify.  One can easily imagine cases 
involving defining constants (in terms of ring operations) that one then 
wants to remain opaque to ring_simplify, so that the result isn't 
over-simplified.

-- Jonathan