Ignore:
Timestamp:
Mar 29, 2013, 12:09:07 PM (8 years ago)
Author:
campbell
Message:

Break up front-end for correctness proof.
Use let rec to prevent labelling function from unfolding.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2722 r3030  
    12741274@(swl_steps E0 E0)
    12751275[ 2: @steps_step | skip | // | @build_exec
    1276   [ @transform_program_gen_related | // | inversion NW
     1276  [ whd in match ge2; >unfold_clight_label @transform_program_gen_related
     1277  | //
     1278  | inversion NW
    12771279    [ #tr #i #s #E1 #E2 destruct
    12781280    | #trX #sX #eX #NWX #E1X #E2X destruct //
Note: See TracChangeset for help on using the changeset viewer.