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/identifiers.ml

    r2730 r2743  
    5151(** val universe_rect_Type4 :
    5252    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    53 let rec universe_rect_Type4 tag h_mk_universe x_1017 =
    54   let next_identifier = x_1017 in h_mk_universe next_identifier
     53let rec universe_rect_Type4 tag h_mk_universe x_3083 =
     54  let next_identifier = x_3083 in h_mk_universe next_identifier
    5555
    5656(** val universe_rect_Type5 :
    5757    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    58 let rec universe_rect_Type5 tag h_mk_universe x_1019 =
    59   let next_identifier = x_1019 in h_mk_universe next_identifier
     58let rec universe_rect_Type5 tag h_mk_universe x_3085 =
     59  let next_identifier = x_3085 in h_mk_universe next_identifier
    6060
    6161(** val universe_rect_Type3 :
    6262    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    63 let rec universe_rect_Type3 tag h_mk_universe x_1021 =
    64   let next_identifier = x_1021 in h_mk_universe next_identifier
     63let rec universe_rect_Type3 tag h_mk_universe x_3087 =
     64  let next_identifier = x_3087 in h_mk_universe next_identifier
    6565
    6666(** val universe_rect_Type2 :
    6767    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    68 let rec universe_rect_Type2 tag h_mk_universe x_1023 =
    69   let next_identifier = x_1023 in h_mk_universe next_identifier
     68let rec universe_rect_Type2 tag h_mk_universe x_3089 =
     69  let next_identifier = x_3089 in h_mk_universe next_identifier
    7070
    7171(** val universe_rect_Type1 :
    7272    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    73 let rec universe_rect_Type1 tag h_mk_universe x_1025 =
    74   let next_identifier = x_1025 in h_mk_universe next_identifier
     73let rec universe_rect_Type1 tag h_mk_universe x_3091 =
     74  let next_identifier = x_3091 in h_mk_universe next_identifier
    7575
    7676(** val universe_rect_Type0 :
    7777    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    78 let rec universe_rect_Type0 tag h_mk_universe x_1027 =
    79   let next_identifier = x_1027 in h_mk_universe next_identifier
     78let rec universe_rect_Type0 tag h_mk_universe x_3093 =
     79  let next_identifier = x_3093 in h_mk_universe next_identifier
    8080
    8181(** val next_identifier :
     
    137137type fresh_for_univ = __
    138138
    139 type env_fresh_for_univ = __
     139type 'x env_fresh_for_univ = __
    140140
    141141(** val eq_identifier :
     
    181181  Positive.succ_pos_of_nat n
    182182
    183 type distinct_env = __
     183type 'x distinct_env = __
    184184
    185185(** val check_member_env :
     
    221221    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    222222    'a1 identifier_map -> 'a2 **)
    223 let rec identifier_map_rect_Type4 tag h_an_id_map x_1044 =
    224   let x_1045 = x_1044 in h_an_id_map x_1045
     223let rec identifier_map_rect_Type4 tag h_an_id_map x_3255 =
     224  let x_3256 = x_3255 in h_an_id_map x_3256
    225225
    226226(** val identifier_map_rect_Type5 :
    227227    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    228228    'a1 identifier_map -> 'a2 **)
    229 let rec identifier_map_rect_Type5 tag h_an_id_map x_1047 =
    230   let x_1048 = x_1047 in h_an_id_map x_1048
     229let rec identifier_map_rect_Type5 tag h_an_id_map x_3258 =
     230  let x_3259 = x_3258 in h_an_id_map x_3259
    231231
    232232(** val identifier_map_rect_Type3 :
    233233    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    234234    'a1 identifier_map -> 'a2 **)
    235 let rec identifier_map_rect_Type3 tag h_an_id_map x_1050 =
    236   let x_1051 = x_1050 in h_an_id_map x_1051
     235let rec identifier_map_rect_Type3 tag h_an_id_map x_3261 =
     236  let x_3262 = x_3261 in h_an_id_map x_3262
    237237
    238238(** val identifier_map_rect_Type2 :
    239239    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    240240    'a1 identifier_map -> 'a2 **)
    241 let rec identifier_map_rect_Type2 tag h_an_id_map x_1053 =
    242   let x_1054 = x_1053 in h_an_id_map x_1054
     241let rec identifier_map_rect_Type2 tag h_an_id_map x_3264 =
     242  let x_3265 = x_3264 in h_an_id_map x_3265
    243243
    244244(** val identifier_map_rect_Type1 :
    245245    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    246246    'a1 identifier_map -> 'a2 **)
    247 let rec identifier_map_rect_Type1 tag h_an_id_map x_1056 =
    248   let x_1057 = x_1056 in h_an_id_map x_1057
     247let rec identifier_map_rect_Type1 tag h_an_id_map x_3267 =
     248  let x_3268 = x_3267 in h_an_id_map x_3268
    249249
    250250(** val identifier_map_rect_Type0 :
    251251    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    252252    'a1 identifier_map -> 'a2 **)
    253 let rec identifier_map_rect_Type0 tag h_an_id_map x_1059 =
    254   let x_1060 = x_1059 in h_an_id_map x_1060
     253let rec identifier_map_rect_Type0 tag h_an_id_map x_3270 =
     254  let x_3271 = x_3270 in h_an_id_map x_3271
    255255
    256256(** val identifier_map_inv_rect_Type4 :
     
    406406   | Types.Some m'0 -> (fun _ -> m'0)) __
    407407
    408 type fresh_for_map = __
     408type 'x fresh_for_map = __
    409409
    410410type identifier_set = Types.unit0 identifier_map
     
    465465  Util.foldl (add_set tag) (empty_set tag)
    466466
     467(** val dpi1__o__id_set_from_list__o__inject :
     468    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list,
     469    'a1) Types.dPair -> Types.unit0 identifier_map Types.sig0 **)
     470let dpi1__o__id_set_from_list__o__inject x0 x3 =
     471  set_from_list x0 x3.Types.dpi1
     472
     473(** val eject__o__id_set_from_list__o__inject :
     474    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
     475    Types.sig0 -> Types.unit0 identifier_map Types.sig0 **)
     476let eject__o__id_set_from_list__o__inject x0 x3 =
     477  set_from_list x0 (Types.pi1 x3)
     478
     479(** val id_set_from_list__o__inject :
     480    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
     481    Types.unit0 identifier_map Types.sig0 **)
     482let id_set_from_list__o__inject x0 x2 =
     483  set_from_list x0 x2
     484
     485(** val dpi1__o__id_set_from_list :
     486    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list,
     487    'a1) Types.dPair -> Types.unit0 identifier_map **)
     488let dpi1__o__id_set_from_list x0 x2 =
     489  set_from_list x0 x2.Types.dpi1
     490
     491(** val eject__o__id_set_from_list :
     492    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
     493    Types.sig0 -> Types.unit0 identifier_map **)
     494let eject__o__id_set_from_list x0 x2 =
     495  set_from_list x0 (Types.pi1 x2)
     496
    467497(** val choose :
    468498    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
Note: See TracChangeset for help on using the changeset viewer.