Changeset 2653 for src/ASM/Policy.ma


Ignore:
Timestamp:
Feb 8, 2013, 1:45:22 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2652 r2653  
    199199   | #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
    200200     whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
    201      normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq; (*320s*)
     201     normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq ⊢ ?; (*320s*)
    202202     #x cases x -x #Sno_ch #Spol normalize nodelta cases Spol
    203203     [ normalize nodelta #HSn #Heq #Seq cases Heq
Note: See TracChangeset for help on using the changeset viewer.