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

    r2730 r2743  
    9898    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    9999    -> classify_add_cases -> 'a1 **)
    100 let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_4059 x_4058 = function
     100let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7350 x_7349 = function
    101101| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    102102| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    110110    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    111111    -> classify_add_cases -> 'a1 **)
    112 let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_4066 x_4065 = function
     112let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7357 x_7356 = function
    113113| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    114114| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    122122    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    123123    -> classify_add_cases -> 'a1 **)
    124 let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_4073 x_4072 = function
     124let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7364 x_7363 = function
    125125| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    126126| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    134134    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    135135    -> classify_add_cases -> 'a1 **)
    136 let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_4080 x_4079 = function
     136let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7371 x_7370 = function
    137137| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    138138| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    146146    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    147147    -> classify_add_cases -> 'a1 **)
    148 let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_4087 x_4086 = function
     148let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7378 x_7377 = function
    149149| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    150150| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    158158    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    159159    -> classify_add_cases -> 'a1 **)
    160 let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_4094 x_4093 = function
     160let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7385 x_7384 = function
    161161| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    162162| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    321321    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    322322    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    323 let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_4150 x_4149 = function
     323let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7441 x_7440 = function
    324324| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    325325| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    333333    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    334334    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    335 let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_4157 x_4156 = function
     335let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7448 x_7447 = function
    336336| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    337337| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    345345    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    346346    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    347 let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_4164 x_4163 = function
     347let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7455 x_7454 = function
    348348| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    349349| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    357357    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    358358    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    359 let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_4171 x_4170 = function
     359let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7462 x_7461 = function
    360360| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    361361| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    369369    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    370370    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    371 let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_4178 x_4177 = function
     371let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7469 x_7468 = function
    372372| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    373373| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    381381    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    382382    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    383 let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_4185 x_4184 = function
     383let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7476 x_7475 = function
    384384| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    385385| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    521521    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    522522    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    523 let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_4239 x_4238 = function
     523let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_7530 x_7529 = function
    524524| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    525525| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    528528    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    529529    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    530 let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_4244 x_4243 = function
     530let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_7535 x_7534 = function
    531531| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    532532| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    535535    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    536536    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    537 let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_4249 x_4248 = function
     537let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_7540 x_7539 = function
    538538| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    539539| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    542542    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    543543    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    544 let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_4254 x_4253 = function
     544let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_7545 x_7544 = function
    545545| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    546546| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    549549    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    550550    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    551 let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_4259 x_4258 = function
     551let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_7550 x_7549 = function
    552552| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    553553| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    556556    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    557557    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    558 let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_4264 x_4263 = function
     558let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_7555 x_7554 = function
    559559| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    560560| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    638638    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    639639    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    640 let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_4305 x_4304 = function
     640let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7596 x_7595 = function
    641641| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    642642| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    647647    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    648648    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    649 let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_4311 x_4310 = function
     649let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7602 x_7601 = function
    650650| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    651651| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    656656    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    657657    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    658 let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_4317 x_4316 = function
     658let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7608 x_7607 = function
    659659| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    660660| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    665665    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    666666    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    667 let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_4323 x_4322 = function
     667let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7614 x_7613 = function
    668668| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    669669| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    674674    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    675675    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    676 let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_4329 x_4328 = function
     676let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7620 x_7619 = function
    677677| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    678678| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    683683    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    684684    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    685 let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_4335 x_4334 = function
     685let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7626 x_7625 = function
    686686| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    687687| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    782782    -> 'a1 **)
    783783let rec classify_fun_cases_rect_Type4 h_fun_case_f h_fun_default = function
    784 | Fun_case_f (x_4383, x_4382) -> h_fun_case_f x_4383 x_4382
     784| Fun_case_f (x_7674, x_7673) -> h_fun_case_f x_7674 x_7673
    785785| Fun_default -> h_fun_default
    786786
     
    789789    -> 'a1 **)
    790790let rec classify_fun_cases_rect_Type5 h_fun_case_f h_fun_default = function
    791 | Fun_case_f (x_4388, x_4387) -> h_fun_case_f x_4388 x_4387
     791| Fun_case_f (x_7679, x_7678) -> h_fun_case_f x_7679 x_7678
    792792| Fun_default -> h_fun_default
    793793
     
    796796    -> 'a1 **)
    797797let rec classify_fun_cases_rect_Type3 h_fun_case_f h_fun_default = function
    798 | Fun_case_f (x_4393, x_4392) -> h_fun_case_f x_4393 x_4392
     798| Fun_case_f (x_7684, x_7683) -> h_fun_case_f x_7684 x_7683
    799799| Fun_default -> h_fun_default
    800800
     
    803803    -> 'a1 **)
    804804let rec classify_fun_cases_rect_Type2 h_fun_case_f h_fun_default = function
    805 | Fun_case_f (x_4398, x_4397) -> h_fun_case_f x_4398 x_4397
     805| Fun_case_f (x_7689, x_7688) -> h_fun_case_f x_7689 x_7688
    806806| Fun_default -> h_fun_default
    807807
     
    810810    -> 'a1 **)
    811811let rec classify_fun_cases_rect_Type1 h_fun_case_f h_fun_default = function
    812 | Fun_case_f (x_4403, x_4402) -> h_fun_case_f x_4403 x_4402
     812| Fun_case_f (x_7694, x_7693) -> h_fun_case_f x_7694 x_7693
    813813| Fun_default -> h_fun_default
    814814
     
    817817    -> 'a1 **)
    818818let rec classify_fun_cases_rect_Type0 h_fun_case_f h_fun_default = function
    819 | Fun_case_f (x_4408, x_4407) -> h_fun_case_f x_4408 x_4407
     819| Fun_case_f (x_7699, x_7698) -> h_fun_case_f x_7699 x_7698
    820820| Fun_default -> h_fun_default
    821821
Note: See TracChangeset for help on using the changeset viewer.