Matthieu Sozeau

@coqbot run full ci

I think the citation should reflect the current system, so I would say 1) yes, with the version number, 2) the release announcement, plus a little chapô of general intro...

Yup, I’ll do that. Le jeu. 16 nov. 2017 à 12:59, Théo Zimmermann a écrit : > I think the citation should reflect the current system, so I would say...

Last time I tried to put the manual on HAL they refused it IIRC, but I can try again, precisely referring to this need.

I had bad experiences trying to put the refman in HAL. And the Zenodo page directly shows the refman, so I thought it was enough too.

Don't we have permanent URLs for the manual these days?

I think we should pursue the idea of having parts of the evar_map trusted somehow to allow the fast one-typechecking phase. The idea would be of an `evar_define : evar_map...

The main issue I see with "tagging" in the evar_map is that EConstr.kind should probably "go through" these evars anyway.

I agree with @ppedrot, we should rather have a global flag, which could be used for example for the new sort-poly prelude.

@stedolan ?