Skip to content
Snippets Groups Projects
Commit e078c510 authored by Sergey Bozhko's avatar Sergey Bozhko :eyes: Committed by Björn Brandenburg
Browse files

Rename arguments of [apply _ with (NAME0 := _)]

From changelog of Coq version 8.15:
Changed: [apply with] does not rename arguments unless using
compatibility flag Apply With Renaming (#13837, fixes #13759, by Gaëtan
Gilbert).

So, this commit replaces all occurrences of [apply L with (NAME0 := V)]
to [apply L with (NAME := V)]
parent 1959a478
No related branches found
No related tags found
1 merge request!184Update to latest Coq 8.15 and mathcomp 1.14
Showing
with 130 additions and 130 deletions
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment