The Coq mailing list

[Jean-Christophe Léchenet <jean-christophe.lechenet AT irisa.fr>]

Note that there is an open issue on Github about the unclear error 
message when you try to manipulate an evar whose name was not manually 
set: https://github.com/coq/coq/issues/4633.

Jean-Christophe

Le 04/12/2018 à 05:06, Jeremy Dawson a écrit :
> Hi,
>
> thanks for all the answers to my previous question.
>
> FWIW, actually simpl seems to rewrite a goal without instantiating evars
>
> Another question about evars:
> given a goal
>
>    Γ1 ++ l ++ A :: Γ2 ++ B :: Γ3 = ?Γ1 ++ ?A :: ?Γ2 ++ ?B :: ?Γ3
>
> how do I instantiate ?A to A and ?B to B?
>
> I've tried
> instantiate (?A := A).
> and
> instantiate (A := A).
> but both those produce error messages.
>
> thanks
>
> Jeremy