Changeset 3481 for LTS


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

Restored more code claimed to be broken.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3480 r3481  
    23862386    cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh'
    23872387    #EQenv_it' ***** #EQtrans
    2388     #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep cases daemon (*CSC: WAS WORKING
     2388    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
    23892389    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
    23902390    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
     
    24352435        ]
    24362436    | whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    2437     ] *)
     2437    ]
    24382438  ]
    24392439| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?;
Note: See TracChangeset for help on using the changeset viewer.