The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 06/10/2016 09:13, Sylvain Boulmé wrote:

> But, when using this tactic inside a Coq module "TestTactic", I get the
> following error message:
> 
> Error: Illegal application:
> The term "Syntax.Var" of type
>  "forall var : Type, var -> Syntax.expr var"
> cannot be applied to the terms
>  "v" : "Type"
>  "r4" : "v"
> The 1st term has type "Type@{TestTactic.1}"
> which should be coercible to "Type@{Syntax.1}".
> 
> 
> How to correct my code above ?

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).

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.

Best regards,

Guillaume