Changeset 2652 for src/ASM/PolicyStep.ma


Ignore:
Timestamp:
Feb 8, 2013, 11:49:55 AM (7 years ago)
Author:
sacerdot
Message:

String type changed definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2317 r2652  
    927927 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    928928 [ >nth_append_first [2: @Hi] lapply (Hsigma_safe i Hi)
    929    inversion (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins #Heq normalize nodelta
     929   inversion (nth i ? prefix 〈None ?, Comment EmptyString〉) #lbl #ins #Heq normalize nodelta
    930930   #Hsafe #dest #Hjump lapply (Hsafe dest Hjump) -Hsafe
    931931   inversion (leb (lookup_def … labels dest 0) i) #Hle normalize nodelta
     
    12011201  [ (* USE: policy_jump_equal → added = 0 (from fold) *)
    12021202    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
    1203     inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     1203    inversion (is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉)))
    12041204    [ #Hj
    12051205      (* USE: policy_increase (from fold) *)
Note: See TracChangeset for help on using the changeset viewer.