Ignore:
Timestamp:
Oct 19, 2011, 11:54:13 AM (8 years ago)
Author:
campbell
Message:

Remove a few old workarounds.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r1369 r1410  
    2626      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z
    2727      whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E
    28       whd in E:(??%?);
    29       >(?:e' = add ?? y id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
     28      whd in E:(??%?); destruct;
    3029      whd >lookup_add_hit % #A destruct
    3130    | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl)
     
    3332      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *)
    3433      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u''
    35       whd in ⊢ (??%? → ?) #E
    36       >(?:e' = add ?? e1 id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
     34      whd in ⊢ (??%? → ?) #E destruct
    3735      @lookup_add_oblivious
    3836      @(IH … E1 ? H)
Note: See TracChangeset for help on using the changeset viewer.