Ssreflect Users Discussion List

[Cyril Cohen <>]

Le 10/10/2012 17:56, Enrico Tassi a écrit :
> On Wed, Oct 10, 2012 at 10:54:47AM -0400, Andrej Bauer wrote:
> Ah OK, not it makes much more sense and looks way more feasible ;-)
>
> And maybe with some coordination we could avoid doing the work 3 times,
> and sime I'm not in Princeton I guess I should let Assia (and Cyril) take
> the leed.
> I can surely help on the .ml4 side, if something needs to be adapted.

Ok I made my dirty things available at
https://github.com/Barbichu/ssrcoq
I really think it is not the good way to do things and I would be happy 
to work with a patched ssreflect in a context where Init has been 
disconnected and at least with the v8.4 (I already miss eta).

I am fully aware that what I did is very ugly, mainly because the hacks 
I did in ssreflect.ml4 but also because of the "noprop.v" file. The 
"noprop.v" file is indeed the quickest solution I found to work (with 
Type instead of Prop) with a Coq in which Init is still automatically 
exported ...
I also had to make a modification in kernel/univ.ml to make the lemma 
nary_congruence work with equalities in Type, which is necessary to make 
the congr tactic work.

But at least it proves that ssreflect can be adapted to work in the 
univalent setting.

Best regards,
--
Cyril