Ssreflect Users Discussion List

[Andrej Bauer <>]

Dear ssreflectors,

at the Institute for Advanced Study there is a special project going
on, part of which is formalization of mathematics. We are at a stage
when we can make some fundamental changes to Coq. In fact, we've
already ripped out the standard library (yes, all of it). We would
like to explore the use of ssreflect tactics (but not the math
components, at least not right now). I personally believe that this
would greatly benefit our project, as ssreflect-style of proof is much
better suited for mathematics than pure Coq. And I bet ssreflect would
also benefit from additional exposure.

It would be tremendously useful to have the ssrefelct source code
avialable on a major public repository, such as github.com. It is my
understanding that the ssreflect license allows us to do so anyway,
but having our own fork of the library would be a waste of effort (as
we could not easily propagate our changes back to you), and in any
case we do not want to do anything without first talking to the
ssreflect people.

So, what are the chances that you would make the ssrefelct library, or
at least the tactics part of it, publicly available on github?

With kind regards,

Andrej Bauer