Changeset 1951 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 16, 2012, 1:28:43 AM (8 years ago)
Author:
sacerdot
Message:

Bug with overloaded names in the context.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1948 r1951  
    973973    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
    974974    try //
    975     destruct(INSTR_PC) <instr_refl whd
     975    -s destruct(INSTR_PC) <instr_refl whd
    976976    try (#absurd normalize in absurd; try destruct(absurd) try %) %
    977977  |9:
     
    10351035  #cm #s normalize nodelta
    10361036  whd in match execute_1; normalize nodelta @pi2
    1037 qed-. (*x Andrea: indexing takes ages here *)
     1037qed.
    10381038
    10391039lemma execute_1_ok_clock:
Note: See TracChangeset for help on using the changeset viewer.