Skip to content
  • Xavier Leroy's avatar
    Revised correctness proof for record_goto · e16f5d1d
    Xavier Leroy authored
    We used to define an instrumented version record_goto' that also
    builds the measure f, prove it correct, then show equivalence with
    record_goto.
    
    The new proofs make do without the instrumented version.  They prove
    strong existence of the measure, as in
    `{ f | branch_map_correct (record_goto fn) f}`.
    e16f5d1d