Changeset 2465


Ignore:
Timestamp:
Nov 14, 2012, 7:17:15 PM (7 years ago)
Author:
campbell
Message:

Remove obsolete comment (runtime functions should be implemented later in
the compiler).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2407 r2465  
    16441644].
    16451645
    1646 (* TODO: move universe generation to higher level once we do runtime function
    1647    generation.  Cheating a bit - we only need the new identifiers to be fresh
    1648    for individual functions. *)
    1649 
    16501646let rec map_partial_All (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → res B)
    16511647  (l:list A) (H:All A P l) on l : res (list B) ≝
Note: See TracChangeset for help on using the changeset viewer.