Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/registerSet.ml

    r2743 r2773  
    33open Exp
    44
     5open Setoids
     6
     7open Monad
     8
     9open Option
     10
    511open Extranat
    612
     
    5662
    5763open Extralib
    58 
    59 open Setoids
    60 
    61 open Monad
    62 
    63 open Option
    6464
    6565open Lists
     
    8787    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    8888    -> register_set -> 'a1 **)
    89 let rec register_set_rect_Type4 h_mk_register_set x_20855 =
    90   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    91     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    92     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    93     rs_from_list = rs_from_list0 } = x_20855
     89let rec register_set_rect_Type4 h_mk_register_set x_16165 =
     90  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
     91    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
     92    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
     93    rs_from_list = rs_from_list0 } = x_16165
    9494  in
    9595  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
     
    102102    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    103103    -> register_set -> 'a1 **)
    104 let rec register_set_rect_Type5 h_mk_register_set x_20857 =
    105   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    106     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    107     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    108     rs_from_list = rs_from_list0 } = x_20857
     104let rec register_set_rect_Type5 h_mk_register_set x_16167 =
     105  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
     106    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
     107    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
     108    rs_from_list = rs_from_list0 } = x_16167
    109109  in
    110110  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
     
    117117    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    118118    -> register_set -> 'a1 **)
    119 let rec register_set_rect_Type3 h_mk_register_set x_20859 =
    120   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    121     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    122     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    123     rs_from_list = rs_from_list0 } = x_20859
     119let rec register_set_rect_Type3 h_mk_register_set x_16169 =
     120  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
     121    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
     122    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
     123    rs_from_list = rs_from_list0 } = x_16169
    124124  in
    125125  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
     
    132132    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    133133    -> register_set -> 'a1 **)
    134 let rec register_set_rect_Type2 h_mk_register_set x_20861 =
    135   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    136     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    137     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    138     rs_from_list = rs_from_list0 } = x_20861
     134let rec register_set_rect_Type2 h_mk_register_set x_16171 =
     135  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
     136    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
     137    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
     138    rs_from_list = rs_from_list0 } = x_16171
    139139  in
    140140  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
     
    147147    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    148148    -> register_set -> 'a1 **)
    149 let rec register_set_rect_Type1 h_mk_register_set x_20863 =
    150   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    151     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    152     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    153     rs_from_list = rs_from_list0 } = x_20863
     149let rec register_set_rect_Type1 h_mk_register_set x_16173 =
     150  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
     151    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
     152    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
     153    rs_from_list = rs_from_list0 } = x_16173
    154154  in
    155155  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
     
    162162    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    163163    -> register_set -> 'a1 **)
    164 let rec register_set_rect_Type0 h_mk_register_set x_20865 =
    165   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    166     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    167     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    168     rs_from_list = rs_from_list0 } = x_20865
     164let rec register_set_rect_Type0 h_mk_register_set x_16175 =
     165  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
     166    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
     167    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
     168    rs_from_list = rs_from_list0 } = x_16175
    169169  in
    170170  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
     
    183183(** val rs_fold0 :
    184184    register_set -> (I8051.register -> 'a1 -> 'a1) -> __ -> 'a1 -> 'a1 **)
    185 let rec rs_fold0 xxx x_20889 x_20890 x_20891 =
     185let rec rs_fold0 xxx x_16199 x_16200 x_16201 =
    186186  (let { rs_empty = x0; rs_singleton = x1; rs_fold = yyy; rs_insert = x2;
    187187     rs_exists = x3; rs_union = x4; rs_subset = x5; rs_to_list = x6;
    188188     rs_from_list = x7 } = xxx
    189189   in
    190   Obj.magic yyy) __ x_20889 x_20890 x_20891
     190  Obj.magic yyy) __ x_16199 x_16200 x_16201
    191191
    192192(** val rs_insert : register_set -> I8051.register -> __ -> __ **)
Note: See TracChangeset for help on using the changeset viewer.