Post #2780916

@mevenlennonbertrand@lipn.info here is a full account of what was found (collaboration between Opus 4.6 and rocq experts): - 3 proofs of false from bugs in the guard checker - 2 proofs of false from bugs in the module system (the second one uses Girard's paradox) - 1 proof of false from a bug in `conversion.ml` - 1 proof of false from a bug in `discharge.ml` (using Hurkens' paradox) - 1 anomaly from a bug in `conversion.ml` - 2 bugs in `cClosure.ml` - 1 bug in `mod_declarations.ml`