Changeset 1599 for src/common/Events.ma


Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (8 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Events.ma

    r1516 r1599  
    2222(*include "Floats.ma".*)
    2323include "common/Values.ma".
    24 include "basics/list.ma".
     24include "basics/lists/list.ma".
    2525include "utilities/extralib.ma".
    2626include "common/CostLabel.ma".
     
    161161  match T' with
    162162  [ Econsinf' t T'' NOTEMPTY ⇒
    163       match split_traceinf' t T'' NOTEMPTY with [ pair e tl ⇒
    164       Econsinf e (traceinf_of_traceinf' tl) ]
     163      let 〈e,tl〉 ≝ split_traceinf' t T'' NOTEMPTY in
     164      Econsinf e (traceinf_of_traceinf' tl)
    165165  ].
    166166
Note: See TracChangeset for help on using the changeset viewer.