Changeset 2797 for extracted/bind_new.ml


Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/bind_new.ml

    r2775 r2797  
    3535    ('a1, 'a2) bind_new -> 'a3 **)
    3636let rec bind_new_rect_Type4 h_bret h_bnew = function
    37 | Bret x_20763 -> h_bret x_20763
    38 | Bnew x_20765 ->
    39   h_bnew x_20765 (fun x_20764 ->
    40     bind_new_rect_Type4 h_bret h_bnew (x_20765 x_20764))
     37| Bret x_20842 -> h_bret x_20842
     38| Bnew x_20844 ->
     39  h_bnew x_20844 (fun x_20843 ->
     40    bind_new_rect_Type4 h_bret h_bnew (x_20844 x_20843))
    4141
    4242(** val bind_new_rect_Type3 :
     
    4444    ('a1, 'a2) bind_new -> 'a3 **)
    4545let rec bind_new_rect_Type3 h_bret h_bnew = function
    46 | Bret x_20775 -> h_bret x_20775
    47 | Bnew x_20777 ->
    48   h_bnew x_20777 (fun x_20776 ->
    49     bind_new_rect_Type3 h_bret h_bnew (x_20777 x_20776))
     46| Bret x_20854 -> h_bret x_20854
     47| Bnew x_20856 ->
     48  h_bnew x_20856 (fun x_20855 ->
     49    bind_new_rect_Type3 h_bret h_bnew (x_20856 x_20855))
    5050
    5151(** val bind_new_rect_Type2 :
     
    5353    ('a1, 'a2) bind_new -> 'a3 **)
    5454let rec bind_new_rect_Type2 h_bret h_bnew = function
    55 | Bret x_20781 -> h_bret x_20781
    56 | Bnew x_20783 ->
    57   h_bnew x_20783 (fun x_20782 ->
    58     bind_new_rect_Type2 h_bret h_bnew (x_20783 x_20782))
     55| Bret x_20860 -> h_bret x_20860
     56| Bnew x_20862 ->
     57  h_bnew x_20862 (fun x_20861 ->
     58    bind_new_rect_Type2 h_bret h_bnew (x_20862 x_20861))
    5959
    6060(** val bind_new_rect_Type1 :
     
    6262    ('a1, 'a2) bind_new -> 'a3 **)
    6363let rec bind_new_rect_Type1 h_bret h_bnew = function
    64 | Bret x_20787 -> h_bret x_20787
    65 | Bnew x_20789 ->
    66   h_bnew x_20789 (fun x_20788 ->
    67     bind_new_rect_Type1 h_bret h_bnew (x_20789 x_20788))
     64| Bret x_20866 -> h_bret x_20866
     65| Bnew x_20868 ->
     66  h_bnew x_20868 (fun x_20867 ->
     67    bind_new_rect_Type1 h_bret h_bnew (x_20868 x_20867))
    6868
    6969(** val bind_new_rect_Type0 :
     
    7171    ('a1, 'a2) bind_new -> 'a3 **)
    7272let rec bind_new_rect_Type0 h_bret h_bnew = function
    73 | Bret x_20793 -> h_bret x_20793
    74 | Bnew x_20795 ->
    75   h_bnew x_20795 (fun x_20794 ->
    76     bind_new_rect_Type0 h_bret h_bnew (x_20795 x_20794))
     73| Bret x_20872 -> h_bret x_20872
     74| Bnew x_20874 ->
     75  h_bnew x_20874 (fun x_20873 ->
     76    bind_new_rect_Type0 h_bret h_bnew (x_20874 x_20873))
    7777
    7878(** val bind_new_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.