Changeset 2743 for extracted/events.ml


Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/events.ml

    r2730 r2743  
    9191    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    9292let rec eventval_rect_Type4 h_EVint = function
    93 | EVint (sz, x_4706) -> h_EVint sz x_4706
     93| EVint (sz, x_5485) -> h_EVint sz x_5485
    9494
    9595(** val eventval_rect_Type5 :
    9696    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    9797let rec eventval_rect_Type5 h_EVint = function
    98 | EVint (sz, x_4709) -> h_EVint sz x_4709
     98| EVint (sz, x_5488) -> h_EVint sz x_5488
    9999
    100100(** val eventval_rect_Type3 :
    101101    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    102102let rec eventval_rect_Type3 h_EVint = function
    103 | EVint (sz, x_4712) -> h_EVint sz x_4712
     103| EVint (sz, x_5491) -> h_EVint sz x_5491
    104104
    105105(** val eventval_rect_Type2 :
    106106    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    107107let rec eventval_rect_Type2 h_EVint = function
    108 | EVint (sz, x_4715) -> h_EVint sz x_4715
     108| EVint (sz, x_5494) -> h_EVint sz x_5494
    109109
    110110(** val eventval_rect_Type1 :
    111111    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    112112let rec eventval_rect_Type1 h_EVint = function
    113 | EVint (sz, x_4718) -> h_EVint sz x_4718
     113| EVint (sz, x_5497) -> h_EVint sz x_5497
    114114
    115115(** val eventval_rect_Type0 :
    116116    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    117117let rec eventval_rect_Type0 h_EVint = function
    118 | EVint (sz, x_4721) -> h_EVint sz x_4721
     118| EVint (sz, x_5500) -> h_EVint sz x_5500
    119119
    120120(** val eventval_inv_rect_Type4 :
     
    161161    eventval -> 'a1) -> event -> 'a1 **)
    162162let rec event_rect_Type4 h_EVcost h_EVextcall = function
    163 | EVcost x_4746 -> h_EVcost x_4746
     163| EVcost x_5525 -> h_EVcost x_5525
    164164| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    165165
     
    168168    eventval -> 'a1) -> event -> 'a1 **)
    169169let rec event_rect_Type5 h_EVcost h_EVextcall = function
    170 | EVcost x_4750 -> h_EVcost x_4750
     170| EVcost x_5529 -> h_EVcost x_5529
    171171| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    172172
     
    175175    eventval -> 'a1) -> event -> 'a1 **)
    176176let rec event_rect_Type3 h_EVcost h_EVextcall = function
    177 | EVcost x_4754 -> h_EVcost x_4754
     177| EVcost x_5533 -> h_EVcost x_5533
    178178| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    179179
     
    182182    eventval -> 'a1) -> event -> 'a1 **)
    183183let rec event_rect_Type2 h_EVcost h_EVextcall = function
    184 | EVcost x_4758 -> h_EVcost x_4758
     184| EVcost x_5537 -> h_EVcost x_5537
    185185| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    186186
     
    189189    eventval -> 'a1) -> event -> 'a1 **)
    190190let rec event_rect_Type1 h_EVcost h_EVextcall = function
    191 | EVcost x_4762 -> h_EVcost x_4762
     191| EVcost x_5541 -> h_EVcost x_5541
    192192| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    193193
     
    196196    eventval -> 'a1) -> event -> 'a1 **)
    197197let rec event_rect_Type0 h_EVcost h_EVextcall = function
    198 | EVcost x_4766 -> h_EVcost x_4766
     198| EVcost x_5545 -> h_EVcost x_5545
    199199| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    200200
Note: See TracChangeset for help on using the changeset viewer.