CVE-2026-72703

CVE-2026-72703 is a soundness flaw in the guard checker of Rocq Prover (introduced in Coq 8.20). The function find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls when determining parameter uniformity for nested mutual fixpoints. When no body calls itself, it incorrec...