I am trying to see whether I could use Ltac2 in place of Ltac1 and I am a bit struggling to find suitable constructs. What is the idiomatic way of creating an evar of a given type in LTac2 (and potentially depending on the current proof context)?
There was a bit of discussion about this in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Creating.20evars.20in.20Ltac2
The thread was about performance but it still shows at least one way of creating an evar :)
Thanks. It did not occur to me that I could just use
open_constr. I was desperately looking at
Ltac2.Constr and failing to see anything remotely useful.
open_constr:(_:$t) does not work. Indeed, it does not create an evar; it creates a casted evar. So, I ended up using the following (ugly) code to create evars:
Ltac2 evar t := let u := open_constr:(_:$t) in match Constr.Unsafe.kind u with | Constr.Unsafe.Cast v _ _ => v | _ => Control.throw Init.Assertion_failure end.
Oh, yeah, I had forgotten to mention that. You can also call
cbv with just
beta on it, IIRC.
But your solution is the best solution, AFAIK
Last updated: Dec 06 2023 at 14:01 UTC