Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (7 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/smallstep.ml

    r2717 r2730  
    161161    'a1 **)
    162162let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    163 | Terminates (x_6848, x_6847) -> h_Terminates x_6848 x_6847
    164 | Diverges x_6849 -> h_Diverges x_6849
    165 | Reacts x_6850 -> h_Reacts x_6850
    166 | Goes_wrong x_6851 -> h_Goes_wrong x_6851
     163| Terminates (x_5329, x_5328) -> h_Terminates x_5329 x_5328
     164| Diverges x_5330 -> h_Diverges x_5330
     165| Reacts x_5331 -> h_Reacts x_5331
     166| Goes_wrong x_5332 -> h_Goes_wrong x_5332
    167167
    168168(** val program_behavior_rect_Type5 :
     
    171171    'a1 **)
    172172let rec program_behavior_rect_Type5 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    173 | Terminates (x_6858, x_6857) -> h_Terminates x_6858 x_6857
    174 | Diverges x_6859 -> h_Diverges x_6859
    175 | Reacts x_6860 -> h_Reacts x_6860
    176 | Goes_wrong x_6861 -> h_Goes_wrong x_6861
     173| Terminates (x_5339, x_5338) -> h_Terminates x_5339 x_5338
     174| Diverges x_5340 -> h_Diverges x_5340
     175| Reacts x_5341 -> h_Reacts x_5341
     176| Goes_wrong x_5342 -> h_Goes_wrong x_5342
    177177
    178178(** val program_behavior_rect_Type3 :
     
    181181    'a1 **)
    182182let rec program_behavior_rect_Type3 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    183 | Terminates (x_6868, x_6867) -> h_Terminates x_6868 x_6867
    184 | Diverges x_6869 -> h_Diverges x_6869
    185 | Reacts x_6870 -> h_Reacts x_6870
    186 | Goes_wrong x_6871 -> h_Goes_wrong x_6871
     183| Terminates (x_5349, x_5348) -> h_Terminates x_5349 x_5348
     184| Diverges x_5350 -> h_Diverges x_5350
     185| Reacts x_5351 -> h_Reacts x_5351
     186| Goes_wrong x_5352 -> h_Goes_wrong x_5352
    187187
    188188(** val program_behavior_rect_Type2 :
     
    191191    'a1 **)
    192192let rec program_behavior_rect_Type2 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    193 | Terminates (x_6878, x_6877) -> h_Terminates x_6878 x_6877
    194 | Diverges x_6879 -> h_Diverges x_6879
    195 | Reacts x_6880 -> h_Reacts x_6880
    196 | Goes_wrong x_6881 -> h_Goes_wrong x_6881
     193| Terminates (x_5359, x_5358) -> h_Terminates x_5359 x_5358
     194| Diverges x_5360 -> h_Diverges x_5360
     195| Reacts x_5361 -> h_Reacts x_5361
     196| Goes_wrong x_5362 -> h_Goes_wrong x_5362
    197197
    198198(** val program_behavior_rect_Type1 :
     
    201201    'a1 **)
    202202let rec program_behavior_rect_Type1 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    203 | Terminates (x_6888, x_6887) -> h_Terminates x_6888 x_6887
    204 | Diverges x_6889 -> h_Diverges x_6889
    205 | Reacts x_6890 -> h_Reacts x_6890
    206 | Goes_wrong x_6891 -> h_Goes_wrong x_6891
     203| Terminates (x_5369, x_5368) -> h_Terminates x_5369 x_5368
     204| Diverges x_5370 -> h_Diverges x_5370
     205| Reacts x_5371 -> h_Reacts x_5371
     206| Goes_wrong x_5372 -> h_Goes_wrong x_5372
    207207
    208208(** val program_behavior_rect_Type0 :
     
    211211    'a1 **)
    212212let rec program_behavior_rect_Type0 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
    213 | Terminates (x_6898, x_6897) -> h_Terminates x_6898 x_6897
    214 | Diverges x_6899 -> h_Diverges x_6899
    215 | Reacts x_6900 -> h_Reacts x_6900
    216 | Goes_wrong x_6901 -> h_Goes_wrong x_6901
     213| Terminates (x_5379, x_5378) -> h_Terminates x_5379 x_5378
     214| Diverges x_5380 -> h_Diverges x_5380
     215| Reacts x_5381 -> h_Reacts x_5381
     216| Goes_wrong x_5382 -> h_Goes_wrong x_5382
    217217
    218218(** val program_behavior_inv_rect_Type4 :
     
    275275(** val semantics_rect_Type4 :
    276276    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    277 let rec semantics_rect_Type4 h_mk_semantics x_7228 =
    278   let { trans = trans0; ge = ge0 } = x_7228 in
     277let rec semantics_rect_Type4 h_mk_semantics x_5709 =
     278  let { trans = trans0; ge = ge0 } = x_5709 in
    279279  h_mk_semantics trans0 __ __ ge0
    280280
    281281(** val semantics_rect_Type5 :
    282282    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    283 let rec semantics_rect_Type5 h_mk_semantics x_7230 =
    284   let { trans = trans0; ge = ge0 } = x_7230 in
     283let rec semantics_rect_Type5 h_mk_semantics x_5711 =
     284  let { trans = trans0; ge = ge0 } = x_5711 in
    285285  h_mk_semantics trans0 __ __ ge0
    286286
    287287(** val semantics_rect_Type3 :
    288288    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    289 let rec semantics_rect_Type3 h_mk_semantics x_7232 =
    290   let { trans = trans0; ge = ge0 } = x_7232 in
     289let rec semantics_rect_Type3 h_mk_semantics x_5713 =
     290  let { trans = trans0; ge = ge0 } = x_5713 in
    291291  h_mk_semantics trans0 __ __ ge0
    292292
    293293(** val semantics_rect_Type2 :
    294294    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    295 let rec semantics_rect_Type2 h_mk_semantics x_7234 =
    296   let { trans = trans0; ge = ge0 } = x_7234 in
     295let rec semantics_rect_Type2 h_mk_semantics x_5715 =
     296  let { trans = trans0; ge = ge0 } = x_5715 in
    297297  h_mk_semantics trans0 __ __ ge0
    298298
    299299(** val semantics_rect_Type1 :
    300300    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    301 let rec semantics_rect_Type1 h_mk_semantics x_7236 =
    302   let { trans = trans0; ge = ge0 } = x_7236 in
     301let rec semantics_rect_Type1 h_mk_semantics x_5717 =
     302  let { trans = trans0; ge = ge0 } = x_5717 in
    303303  h_mk_semantics trans0 __ __ ge0
    304304
    305305(** val semantics_rect_Type0 :
    306306    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
    307 let rec semantics_rect_Type0 h_mk_semantics x_7238 =
    308   let { trans = trans0; ge = ge0 } = x_7238 in
     307let rec semantics_rect_Type0 h_mk_semantics x_5719 =
     308  let { trans = trans0; ge = ge0 } = x_5719 in
    309309  h_mk_semantics trans0 __ __ ge0
    310310
     
    357357    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    358358    'a1 **)
    359 let rec related_semantics_rect_Type4 h_mk_related_semantics x_7257 =
    360   let { sem1 = sem3; sem2 = sem4 } = x_7257 in
     359let rec related_semantics_rect_Type4 h_mk_related_semantics x_5738 =
     360  let { sem1 = sem3; sem2 = sem4 } = x_5738 in
    361361  h_mk_related_semantics sem3 sem4 __ __ __
    362362
     
    364364    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    365365    'a1 **)
    366 let rec related_semantics_rect_Type5 h_mk_related_semantics x_7259 =
    367   let { sem1 = sem3; sem2 = sem4 } = x_7259 in
     366let rec related_semantics_rect_Type5 h_mk_related_semantics x_5740 =
     367  let { sem1 = sem3; sem2 = sem4 } = x_5740 in
    368368  h_mk_related_semantics sem3 sem4 __ __ __
    369369
     
    371371    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    372372    'a1 **)
    373 let rec related_semantics_rect_Type3 h_mk_related_semantics x_7261 =
    374   let { sem1 = sem3; sem2 = sem4 } = x_7261 in
     373let rec related_semantics_rect_Type3 h_mk_related_semantics x_5742 =
     374  let { sem1 = sem3; sem2 = sem4 } = x_5742 in
    375375  h_mk_related_semantics sem3 sem4 __ __ __
    376376
     
    378378    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    379379    'a1 **)
    380 let rec related_semantics_rect_Type2 h_mk_related_semantics x_7263 =
    381   let { sem1 = sem3; sem2 = sem4 } = x_7263 in
     380let rec related_semantics_rect_Type2 h_mk_related_semantics x_5744 =
     381  let { sem1 = sem3; sem2 = sem4 } = x_5744 in
    382382  h_mk_related_semantics sem3 sem4 __ __ __
    383383
     
    385385    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    386386    'a1 **)
    387 let rec related_semantics_rect_Type1 h_mk_related_semantics x_7265 =
    388   let { sem1 = sem3; sem2 = sem4 } = x_7265 in
     387let rec related_semantics_rect_Type1 h_mk_related_semantics x_5746 =
     388  let { sem1 = sem3; sem2 = sem4 } = x_5746 in
    389389  h_mk_related_semantics sem3 sem4 __ __ __
    390390
     
    392392    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
    393393    'a1 **)
    394 let rec related_semantics_rect_Type0 h_mk_related_semantics x_7267 =
    395   let { sem1 = sem3; sem2 = sem4 } = x_7267 in
     394let rec related_semantics_rect_Type0 h_mk_related_semantics x_5748 =
     395  let { sem1 = sem3; sem2 = sem4 } = x_5748 in
    396396  h_mk_related_semantics sem3 sem4 __ __ __
    397397
     
    449449(** val order_sim_rect_Type4 :
    450450    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    451 let rec order_sim_rect_Type4 h_mk_order_sim x_7288 =
    452   let sem = x_7288 in h_mk_order_sim sem __ __
     451let rec order_sim_rect_Type4 h_mk_order_sim x_5769 =
     452  let sem = x_5769 in h_mk_order_sim sem __ __
    453453
    454454(** val order_sim_rect_Type5 :
    455455    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    456 let rec order_sim_rect_Type5 h_mk_order_sim x_7290 =
    457   let sem = x_7290 in h_mk_order_sim sem __ __
     456let rec order_sim_rect_Type5 h_mk_order_sim x_5771 =
     457  let sem = x_5771 in h_mk_order_sim sem __ __
    458458
    459459(** val order_sim_rect_Type3 :
    460460    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    461 let rec order_sim_rect_Type3 h_mk_order_sim x_7292 =
    462   let sem = x_7292 in h_mk_order_sim sem __ __
     461let rec order_sim_rect_Type3 h_mk_order_sim x_5773 =
     462  let sem = x_5773 in h_mk_order_sim sem __ __
    463463
    464464(** val order_sim_rect_Type2 :
    465465    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    466 let rec order_sim_rect_Type2 h_mk_order_sim x_7294 =
    467   let sem = x_7294 in h_mk_order_sim sem __ __
     466let rec order_sim_rect_Type2 h_mk_order_sim x_5775 =
     467  let sem = x_5775 in h_mk_order_sim sem __ __
    468468
    469469(** val order_sim_rect_Type1 :
    470470    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    471 let rec order_sim_rect_Type1 h_mk_order_sim x_7296 =
    472   let sem = x_7296 in h_mk_order_sim sem __ __
     471let rec order_sim_rect_Type1 h_mk_order_sim x_5777 =
     472  let sem = x_5777 in h_mk_order_sim sem __ __
    473473
    474474(** val order_sim_rect_Type0 :
    475475    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
    476 let rec order_sim_rect_Type0 h_mk_order_sim x_7298 =
    477   let sem = x_7298 in h_mk_order_sim sem __ __
     476let rec order_sim_rect_Type0 h_mk_order_sim x_5779 =
     477  let sem = x_5779 in h_mk_order_sim sem __ __
    478478
    479479(** val sem : order_sim -> related_semantics **)
Note: See TracChangeset for help on using the changeset viewer.