Changeset 3480 for LTS/Language.ma
- Timestamp:
- Sep 22, 2014, 5:27:13 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Language.ma
r3479 r3480 1913 1913 ] 1914 1914 ] 1915 #seq1 #opt_l #i' #_ #EQcode_s1' cases daemon (*CSC: ROTTO QUI1915 #seq1 #opt_l #i' #_ #EQcode_s1' 1916 1916 change with (m_bind ?????) in ⊢ (??%? → ?); 1917 1917 inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct] … … 1942 1942 cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % // 1943 1943 ]] 1944 %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct *)1944 %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct 1945 1945 | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12 1946 1946 #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.