What's the best way to evar-normalize a term in Ltac2? Importantly, it should not reduce beta-redexes, should not remove vm casts nor native casts, and should not incur the overhead of typechecking the term.
I don't think there's such an api around
Does Constr.Unsafe.check
evar-normalize? eval cbv delta [id]
?
(The context of this is https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Debugging.20cyclicly.20defined.20evars)
if you want some hack maybe
Well, it seems that switching from Control.refine
to Control.new_goal
fixes my problem in any case
Last updated: Dec 07 2023 at 04:02 UTC