Test, changelog

Author: yannl35133

doc/changelog/01-kernel/21846-guard-fix-neutral-Added.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  Treat looping fixpoints as branchless matches as fixpoint subterms
+  (`#21846 <https://github.com/rocq-prover/rocq/pull/21846>`_,
+  fixes `#19547 <https://github.com/rocq-prover/rocq/issues/19547>`_,
+  by Yann Leray).

test-suite/success/fixpoint_loop_deadcode.v

@@ -0,0 +1,10 @@
+(* cf. https://github.com/rocq-prover/rocq/issues/19547 *)
+
+Inductive Box (A : Type) : Type := box (a : A).
+Inductive P : Set := PRec : P -> P.
+
+Fixpoint rec (X : P) : False :=
+  let boxP : Box P := (fix loop (p : P) : Box P := match p with PRec p' => loop p' end) X in
+  match boxP with
+  | box _ p => rec p
+  end.