Changeset 3480 for LTS


Ignore:
Timestamp:
Sep 22, 2014, 5:27:13 PM (5 years ago)
Author:
sacerdot
Message:

Restored code claimed to be no longer working.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3479 r3480  
    19131913      ]
    19141914    ]
    1915     #seq1 #opt_l #i' #_ #EQcode_s1' cases daemon (*CSC: ROTTO QUI
     1915    #seq1 #opt_l #i' #_ #EQcode_s1'
    19161916    change with (m_bind ?????) in ⊢ (??%? → ?);
    19171917    inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct]
     
    19421942          cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
    19431943      ]]
    1944     %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct *)
     1944    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    19451945  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    19461946    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
Note: See TracChangeset for help on using the changeset viewer.