Changeset 3481

Timestamp:

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

Author:

sacerdot

Message:

Restored more code claimed to be broken.

File:

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

LTS/Language.ma

@@ -2386 +2386 @@
     cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' 
     #EQenv_it' ***** #EQtrans 
-    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep cases daemon (*CSC: WAS WORKING
+    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
     change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
     [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
@@ -2435 +2435 @@
         ]
     | whd in ⊢ (??%% → ?); #EQ destruct(EQ)
-    ] *)
+    ]
   ]
 | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?;