New operation : Rename Label.
Based on Compcert 3.4 (Coq 8.8.1).
Available operations :
- Rename Global Variable.
- Remove Local Variable (from version 0.7).
- Rename Label (new).
Based on CompCert 2.7.1 and Coq 8.5.2.
New refactoring operation : add/remove a local variable, by Igor Zhirkov.
Proof of correctness for renaming global variables is better structured :
Correspondences between semantic constructions in programs (contexts, continuations, states...) are now represented by relations and not by functions anymore. Proofs are easier, in particular for context transformation, which needed a painful encoding before, and for continuation transformation, which was too memory and time consuming.
More iterators are used to ditinguish properties coming from renaming and those coming from tree traversals.