The Coq mailing list

[Ike Mulder <i.mulder AT cs.ru.nl>]

Hey Abhishek,

You can just do something like `(unify the_evar (some_function the_variable)) || other_case`. If the variable is not in the context of the evar, unify will fail and trigger execution of the other_case branch. You could also wrap the unify call in an 'assert_succeeds' if you only want to check, not actually unify.

If you are using Ltac2, you can also extract this information directly from an evar. The array of constrs in the Evar constructor contain terms (usually variables) that were in scope when the evar was created. (If variables have been rewritten in the mean time, some of them might not be variables anymore.)
To get access to this array, you need to do something like
`match Constr.Unsafe.kind the_evar with
  | Constr.Unsafe.Evar e cs => <your code here>
  | _ => Control.throw Not_found
  end`

Hope this helps! Ike

On 21-09-2023 19:49, Abhishek Anand wrote:

Is there a way to check whether a variable is in the context of an evar?

In my use case, I am trying to instantiate the evar and if the variable is not in context of the evar, I need to first make it existentially quantified.

-- Abhishek

http://www.cs.cornell.edu/~aa755/