The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT imag.fr>]

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.