Changeset 3480 for LTS/Language.ma

Timestamp:

Sep 22, 2014, 5:27:13 PM (5 years ago)

Author:

sacerdot

Message:

Restored code claimed to be no longer working.

File:

• LTS/Language.ma (modified) (2 diffs)

LTS/Language.ma

@@ -1913 +1913 @@
       ]
     ]
-    #seq1 #opt_l #i' #_ #EQcode_s1' cases daemon (*CSC: ROTTO QUI
+    #seq1 #opt_l #i' #_ #EQcode_s1'
     change with (m_bind ?????) in ⊢ (??%? → ?);
     inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct]
@@ -1942 +1942 @@
           cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
       ]]
-    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct *)
+    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
   | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
     #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t