Tags give the ability to mark specific points in history as being important
  • Version-0.8
    Release Version-0.8

    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).
  • Version-0.7
    Release Version-0.7

    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.