I switched a piece of Ltac2 from Std.eval_lazy
to 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 whrec
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: Jun 08 2023 at 04:01 UTC