Changeset 1296


Ignore:
Timestamp:
Oct 5, 2011, 5:53:54 PM (8 years ago)
Author:
mulligan
Message:

changes

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1293 r1296  
    10121012
    10131013(* XXX: following conversation with CSC about the mix up in extension statements
    1014         and extension instructions in RTL *)
     1014        and extension instructions in RTL, use fake_label in calls to
     1015        tailcall_* instructions. *)
    10151016definition translate_stmt ≝
    10161017  λglobals: list ident.
  • src/utilities/adt/table_adt.ma

    r1285 r1296  
    112112        match lr return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
    113113        [ empty ⇒ λabsurd. ?
    114         | node _ lrv lrd lrl lrr ⇒ λ
     114        | node _ lrv lrd lrl lrr ⇒ λnon_empty_proof.
    115115            tbl_create … (tbl_create … ll lv ld lrl) lrv lrd (tbl_create … lrr key val right)
    116         ]
     116        ] ?
    117117    ] left_proof
    118118  | false ⇒ ?
    119119  ].
    120120  [1: normalize in absurd;
     121      elim absurd
     122      #ABSURD
     123      @⊥ @ABSURD @I
     124  |3: normalize in absurd;
    121125      elim absurd
    122126      #ABSURD
Note: See TracChangeset for help on using the changeset viewer.