Stream: Ltac2

Topic: evar normalization

view this post on Zulip Jason Gross (Oct 06 2022 at 13:49):

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.

view this post on Zulip Gaëtan Gilbert (Oct 06 2022 at 14:49):

I don't think there's such an api around

view this post on Zulip Jason Gross (Oct 06 2022 at 15:17):

Does Constr.Unsafe.check evar-normalize? eval cbv delta [id]?

view this post on Zulip Jason Gross (Oct 06 2022 at 15:18):

(The context of this is https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Debugging.20cyclicly.20defined.20evars)

view this post on Zulip Gaëtan Gilbert (Oct 06 2022 at 15:22):

if you want some hack maybe

view this post on Zulip Jason Gross (Oct 06 2022 at 15:41):

Well, it seems that switching from Control.refine to Control.new_goal fixes my problem in any case

Last updated: Apr 20 2024 at 03:40 UTC