I switched a piece of Ltac2 from
Std.eval_cbn and the tactic now raises a
Not_found anomaly in
Raised at file "kernel/environ.ml", line 162, characters 29-44 Called from file "engine/eConstr.ml" (inlined), line 723, characters 51-67 Called from file "pretyping/reductionops.ml", line 981, characters 13-29
(This is Coq 8.12.1). The corresponding code is the
Rel branch of a match on a constr in
whd_state_gen. How do I go about debugging this?
Oh, maybe I have unbound rels in my term. I guess
lazy doesn't care about that?
lazy is probably more resilient than cbn indeed
Ugh, indeed.. unbound rels hidden in implicit arguments. I guess that settles it.
Last updated: Dec 07 2023 at 09:01 UTC