I stumbled upon a strange interaction of pose with change on an inductive in SProp:
Inductive P : SProp := C.
Goal forall (f : P -> Type) (x : P), f x.
intros f x.
(* Works as expected *)
Fail Fail change x with C.
pose (t := C).
(* Does not work ??? *)
Fail change x with t.
(* Works if we explicitly unfold *)
let tu := eval unfold t in t in change x with tu.
I am not sure were the problem is coming from and I didn't find a corresponding issue on github, should I open one ?
cc @Gaëtan Gilbert
classic bad relevance
it may be possible to get pose to generate correct relevance so worth an issue imo
A way to print the relevances in debug mode would be appreciated btw.
See https://github.com/coq/coq/pull/15090.
Incidentally this fixes the issue I was mentioning last lunch with my descent into madness with prefascist CwFs
Filed an issue to keep track of this https://github.com/coq/coq/issues/15091
Last updated: Dec 01 2023 at 07:01 UTC