Mentions légales du service

Skip to content

Change a rewrite with wrong occurrence numbers

HERBELIN Hugo requested to merge herbelin/interval:master+adapt13568-invalid-occurrences-rewrite into master

Hi, there is an ongoing Coq PR #13568, which may eventually give an error when using rewrite with wrong occurrence numbers.

This interval MR updates such a rewrite.

It is backward compatible and can be merged now.

Merge request reports