Pierre Castéran

> maybe giving the possibility to display only the assumptions that have changed would be nice Giving options like (all-hyps -hyp1 -hyp2 ... ) or (no-hyps + hyp1 +hyp2 ......

Ok, I see! For my part, I’m working on using Alectryon for writing a pdf document. When commenting the main steps of a long proof, I often present some sub-goal,...

Hi, Indeed it looks to be a problem with Macports. Pierre > port select --summary Name Selected Options ==== ======== ======= python none base.mp_1642503235 none.mp_1642503235 python25-apple none python3 none none...

> > Are you on Apple (M1) silicon? > > No, it’s still an Intel processor > — > Reply to this email directly, view it on GitHub , or...

I would like to include goedel (and its helper pocklington) contrib in the list. The current version available in coq-contribs is for Coq8.10. The first incompatibilities I noticed were :...

@palmskog Done, but I wonder why Hint Rewrite doesn't accept locality attribute. Thus, the Hint Rewrite commands are left unchanged.

Attempt to progressively incorporate some Stdpp style (type classes). @palmskog If you agree, we may merge it into master

Yes, I will try to understand which lemma should remain or made opaque (or simply not being unfolded) in Goedel. Meanwhile, I will maintain two branches in hydra-battles.

@palmskog I'd a look at your experimental branch. That's much better ! Thanks !

Since the pdf is now made with Alectryon, we won't have to update too much the latex files, except for a link to Bas Spitter and van der Weegen's article...