The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

If you want to be minimal in the typing you do and know where new universe constraints

should appear, you can also call Evd.set_(l)eq_sort to generate the appropriate constraints.

Cheers,

-- Matthieu

On Thu, Oct 6, 2016 at 11:33 AM Sylvain Boulmé <Sylvain.Boulme AT imag.fr> wrote:

Thanks a lot Guillaume,

Le 06/10/2016 à 09:22, Guillaume Melquiond a écrit :

> As far as I know, you are supposed to call Typing.type_of on your newly
> created term. That will return a new evarmap that should pass to
> tclEVARS rather than the old one (which does not contain enough universe
> constraints for checking that your new term is well-typed).

Yes, applying this solve my issue.

> Unfortunately, it means type-checking your term twice, which you
> precisely wanted to avoid since you are calling exact_no_check. Another
> solution is thus not too call Typing.type_of on your new term, but on a
> smaller simpler dummy term. If your dummy term (whatever its type)
> happens to produce the exact same universe constraints as your new term,
> then you are good to go and you can use the produced evarmap instead.
>

This very smart trick seems also to work very well ;-)

Thanks again !

Sylvain.