Changeset 1481


Ignore:
Timestamp:
Nov 2, 2011, 2:00:16 PM (8 years ago)
Author:
sacerdot
Message:

Proof fixed. The new standard library does not index any longer the lemma
previously used. However, automation should be equally successfull. The reason
it is not is because it does not handle let-ins correctly.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r1450 r1481  
    248248  let stack_params ≝ \snd hdw_stack_params in
    249249    set_params_hdw globals hdw_params @ set_params_stack globals stack_params.
    250 /2/
     250normalize nodelta /2/
    251251qed.
    252252
Note: See TracChangeset for help on using the changeset viewer.