[Iris-Club] Installing Iris Coq mode on Windows

[Ralf Jung]

Hello again Jan,

>> On a slightly unrelated note: I saw here
>> (https://coq.inria.fr/distrib/current/refman/ssreflect.html) that since
>> version 8.7 Ssreflect is a native part of Coq. However just compiling
>> without additionally installing Ssreflect from the mathematical
>> components library did not work. Are there any plans to switch from the
>> external Ssreflect library to the one that is part of Coq in the future?
> 
> Iris master currently still supports Coq 8.6.1, which is why is still uses the
> "external" ssreflect.  But yes, this switch will happen.  In fact it already
> happened in the "gen_proofmode" branch that we are currently working on.  We
> don't have an ETA for merging that into master, but I hope it happens Soon (TM).

Iris master now depends on Coq 8.7, and we have dropped the dependency on
ssreflect.  Probably too late for you, sorry, but when/if you do an update you
don't have to worry about ssreflect any more.

; Ralf