Development Log

  • SPARK Pro
    May 3rd, 2017

    Use unique names for private record parts
    GNATprove now generates unique names for the Why3 translation of private parts of distinct record types. This should facilitate mappings of these parts to distinct types in interactive theorem provers.