Changeset 2716


Ignore:
Timestamp:
Feb 23, 2013, 1:03:15 AM (6 years ago)
Author:
sacerdot
Message:

utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction

Location:
src
Files:
4 edited
1 moved

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostCheck.ma

    r2601 r2716  
    2525] qed.
    2626
    27 include alias "utilities/deqsets.ma".
     27include alias "utilities/deqsets_extras.ma".
    2828
    2929lemma successors_present : ∀g,st.
     
    235235qed.
    236236
    237 include alias "utilities/deqsets.ma".
     237include alias "utilities/deqsets_extras.ma".
    238238
    239239lemma after_branch_are_cost_labels : ∀g. ∀CL:graph_closed g.
  • src/RTLabs/RTLabs_abstract.ma

    r2677 r2716  
    1010include "common/StructuredTraces.ma".
    1111include "RTLabs/CostSpec.ma". (* TODO: relocate definitions? *)
    12 include "utilities/deqsets.ma".
     12include "utilities/deqsets_extras.ma".
    1313discriminator status_class.
    1414
  • src/RTLabs/RTLabs_traces.ma

    r2677 r2716  
    23072307qed.
    23082308
    2309 include alias "utilities/deqsets.ma".
     2309include alias "utilities/deqsets_extras.ma".
    23102310
    23112311(* Build the tail of the "bad" loop using the reappearance of the original pc,
  • src/joint/TranslateUtils.ma

    r2708 r2716  
    22include "joint/blocks.ma".
    33include "utilities/hide.ma".
    4 include "utilities/deqsets.ma".
     4include "utilities/deqsets_extras.ma".
    55
    66(*include alias "basics/lists/list.ma".
Note: See TracChangeset for help on using the changeset viewer.