Changeset 3482 for LTS/Language.ma

Timestamp:

Sep 22, 2014, 5:46:31 PM (6 years ago)

Author:

sacerdot

Message:

No more daemons, all code repaired.

File:

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

LTS/Language.ma

@@ -2503 +2503 @@
     lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
     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
@@ -2549 +2549 @@
        | * [|#x1] #EQ destruct normalize nodelta whd in ⊢ (??%% → ?);
          #EQ destruct ****** [2: *] #EQ destruct
-       | #EQ whd in ⊢ (??%% → ?); #EQ1 destruct *****
        ]
      ]