The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/31/2014 02:13 PM, Maxime Dénès wrote:
> Hello Xavier,
>
> You're raising an important issue, and I guess most users and 
> developers agree that basic Coq tactics desperately need some love.
>
> I see two main reasons why this is not happening more:
> - The usual argument: the academic system does not reward such work as 
> it is very hard to publish. So spending time on it, at least for young 
> researchers, is very risky due to peer pressure to publish, and the 
> low number of positions.

True, but aren't the institutions involved in the development of Coq not 
purely academic?

> - Some well thought design decisions were already taken and 
> implemented in ssreflect's tactics, which leaves little incentive to 
> re-implement them.

After this discussion, as well as some former ones (such as about 
automatic hypothesis naming), I am going to look at SSReflect.  But I 
have several questions:

- Is there access to a development version that works with the trunk 
version of Coq?

- As I recall, SSReflect relies considerably on revert/re-intro style 
patterns.  Do the SSReflect versions of these destroy evar 
instantiability as they do in vanilla Coq?  I have been learning how to 
write Ltac tactics that don't alter the context to the point where evars 
become uninstantiable (as well as others that try to prevent 
uninstatiability) - and it seems like SSReflect's style could make this 
harder rather than easier.  Or, does SSReflect have ways around this 
already?

-- Jonathan