Changeset 1951

Show
Ignore:
Timestamp:
05/16/12 01:28:43 (12 months ago)
Author:
sacerdot
Message:

Bug with overloaded names in the context.

Files:
1 modified

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: