Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • classic-prosa
  • wip-hunspell
  • prepare_MC_PR
  • tutorial
  • fset
  • embed_arr_seq_uniq
  • v0.5
  • v0.4
  • v0.3
  • v0.2
  • v0.1
12 results
Blame Permalink
Forked from RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
Source project has a limited visibility.
  • Sergey Bozhko's avatar
    e078c510
    Rename arguments of [apply _ with (NAME0 := _)] · e078c510
    Sergey Bozhko authored and Björn Brandenburg's avatar Björn Brandenburg committed 
    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)]
    e078c510
    History
    Rename arguments of [apply _ with (NAME0 := _)]
    Sergey Bozhko authored and Björn Brandenburg's avatar Björn Brandenburg committed 
    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)]