Change a rewrite with wrong occurrence numbers (!4) · Merge requests · CoqInterval / interval · GitLab

Mentions légales du service

La vérification des quotas de chaque projet est mise en place en mode non bloquant. Plus d'information sur : https://doc-si.inria.fr/pages/viewpage.action?pageId=146834656
Quota verification is enabled for projects in non-blocking mode. More information: https://doc-si.inria.fr/pages/viewpage.action?pageId=146834656

Mise à jour GitLab terminée. Nous sommes désormais en version 17.6.1 : https://about.gitlab.com/releases/2024/11/21/gitlab-17-6-released/

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

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.