Changeset 2000


Ignore:
Timestamp:
May 25, 2012, 11:01:49 AM (5 years ago)
Author:
campbell
Message:

Fix g.e. glitch in label simulation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r1986 r2000  
    711711      whd in EX:(??%?);
    712712      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
    713       [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list ? m (blocks_of_env e)))}
     713      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))}
    714714        % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
    715715        | // ] | /3/ ]
Note: See TracChangeset for help on using the changeset viewer.