Changeset 2977 for extracted/rTL.ml


Ignore:
Timestamp:
Mar 27, 2013, 4:09:56 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after several bug fixes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTL.ml

    r2961 r2977  
    125125    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    126126let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
    127 | Rtl_stack_address (x_7, x_6) -> h_rtl_stack_address x_7 x_6
     127| Rtl_stack_address (x_1495, x_1494) -> h_rtl_stack_address x_1495 x_1494
    128128
    129129(** val rtl_seq_rect_Type5 :
    130130    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    131131let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
    132 | Rtl_stack_address (x_11, x_10) -> h_rtl_stack_address x_11 x_10
     132| Rtl_stack_address (x_1499, x_1498) -> h_rtl_stack_address x_1499 x_1498
    133133
    134134(** val rtl_seq_rect_Type3 :
    135135    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    136136let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
    137 | Rtl_stack_address (x_15, x_14) -> h_rtl_stack_address x_15 x_14
     137| Rtl_stack_address (x_1503, x_1502) -> h_rtl_stack_address x_1503 x_1502
    138138
    139139(** val rtl_seq_rect_Type2 :
    140140    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    141141let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
    142 | Rtl_stack_address (x_19, x_18) -> h_rtl_stack_address x_19 x_18
     142| Rtl_stack_address (x_1507, x_1506) -> h_rtl_stack_address x_1507 x_1506
    143143
    144144(** val rtl_seq_rect_Type1 :
    145145    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    146146let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
    147 | Rtl_stack_address (x_23, x_22) -> h_rtl_stack_address x_23 x_22
     147| Rtl_stack_address (x_1511, x_1510) -> h_rtl_stack_address x_1511 x_1510
    148148
    149149(** val rtl_seq_rect_Type0 :
    150150    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    151151let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
    152 | Rtl_stack_address (x_27, x_26) -> h_rtl_stack_address x_27 x_26
     152| Rtl_stack_address (x_1515, x_1514) -> h_rtl_stack_address x_1515 x_1514
    153153
    154154(** val rtl_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.