The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Thu, Jul 31, 2014 at 04:28:31PM -0400, Jonathan wrote:
> - Is there access to a development version that works with the trunk version
> of Coq?

It is there:
  
https://gforge.inria.fr/scm/viewvc.php/trunk/Saclay/Ssreflect/?root=coq-contribs

But don't use it in "production"

> - 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?

I'm not sure I understand what you mean by destroy evar instantiability.

Ssr POV is that evars are constants, no ssr tactic should let you
instantiate them, but should not "destroy" them either.  We hardly use
evars in our goals.
Ssr is not just a set of tactics, but also a formalization style, and
learning the latter is harder than learning the tactic language.

Best,
-- 
Enrico Tassi