Changeset 1946 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 15, 2012, 12:01:30 AM (9 years ago)
Author:
sacerdot
Message:

\snd half_add => add everywhere

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1939 r1946  
    905905        (λx. λs.
    906906        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    907         [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
     907        [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
    908908        | _ ⇒ λabsd. ⊥
    909909        ] (subaddressing_modein … x)) instr' s
     
    987987        (λx. λs.
    988988        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    989         [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
     989        [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
    990990        | _ ⇒ λabsd. ⊥
    991991        ] (subaddressing_modein … x)) instr' s) try @absd
Note: See TracChangeset for help on using the changeset viewer.