Changeset 2743 for extracted/eRTL.ml


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

    r2730 r2743  
    112112    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    113113let rec move_dst_rect_Type4 h_PSD h_HDW = function
    114 | PSD x_147 -> h_PSD x_147
    115 | HDW x_148 -> h_HDW x_148
     114| PSD x_20901 -> h_PSD x_20901
     115| HDW x_20902 -> h_HDW x_20902
    116116
    117117(** val move_dst_rect_Type5 :
    118118    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    119119let rec move_dst_rect_Type5 h_PSD h_HDW = function
    120 | PSD x_152 -> h_PSD x_152
    121 | HDW x_153 -> h_HDW x_153
     120| PSD x_20906 -> h_PSD x_20906
     121| HDW x_20907 -> h_HDW x_20907
    122122
    123123(** val move_dst_rect_Type3 :
    124124    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    125125let rec move_dst_rect_Type3 h_PSD h_HDW = function
    126 | PSD x_157 -> h_PSD x_157
    127 | HDW x_158 -> h_HDW x_158
     126| PSD x_20911 -> h_PSD x_20911
     127| HDW x_20912 -> h_HDW x_20912
    128128
    129129(** val move_dst_rect_Type2 :
    130130    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    131131let rec move_dst_rect_Type2 h_PSD h_HDW = function
    132 | PSD x_162 -> h_PSD x_162
    133 | HDW x_163 -> h_HDW x_163
     132| PSD x_20916 -> h_PSD x_20916
     133| HDW x_20917 -> h_HDW x_20917
    134134
    135135(** val move_dst_rect_Type1 :
    136136    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    137137let rec move_dst_rect_Type1 h_PSD h_HDW = function
    138 | PSD x_167 -> h_PSD x_167
    139 | HDW x_168 -> h_HDW x_168
     138| PSD x_20921 -> h_PSD x_20921
     139| HDW x_20922 -> h_HDW x_20922
    140140
    141141(** val move_dst_rect_Type0 :
    142142    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    143143let rec move_dst_rect_Type0 h_PSD h_HDW = function
    144 | PSD x_172 -> h_PSD x_172
    145 | HDW x_173 -> h_HDW x_173
     144| PSD x_20926 -> h_PSD x_20926
     145| HDW x_20927 -> h_HDW x_20927
    146146
    147147(** val move_dst_inv_rect_Type4 :
     
    195195  Joint.Reg x
    196196
     197(** val dpi1__o__move_dst_to_src__o__inject :
     198    (move_dst, 'a1) Types.dPair -> move_src Types.sig0 **)
     199let dpi1__o__move_dst_to_src__o__inject x2 =
     200  move_src_from_dst x2.Types.dpi1
     201
     202(** val eject__o__move_dst_to_src__o__inject :
     203    move_dst Types.sig0 -> move_src Types.sig0 **)
     204let eject__o__move_dst_to_src__o__inject x2 =
     205  move_src_from_dst (Types.pi1 x2)
     206
     207(** val move_dst_to_src__o__inject : move_dst -> move_src Types.sig0 **)
     208let move_dst_to_src__o__inject x1 =
     209  move_src_from_dst x1
     210
     211(** val dpi1__o__move_dst_to_src :
     212    (move_dst, 'a1) Types.dPair -> move_src **)
     213let dpi1__o__move_dst_to_src x1 =
     214  move_src_from_dst x1.Types.dpi1
     215
     216(** val eject__o__move_dst_to_src : move_dst Types.sig0 -> move_src **)
     217let eject__o__move_dst_to_src x1 =
     218  move_src_from_dst (Types.pi1 x1)
     219
    197220(** val psd_argument_move_src : Joint.psd_argument -> move_src **)
    198221let psd_argument_move_src = function
    199222| Joint.Reg r -> Joint.Reg (PSD r)
    200223| Joint.Imm b -> Joint.Imm b
     224
     225(** val byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
     226    BitVector.byte -> move_src Types.sig0 **)
     227let byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x0 =
     228  psd_argument_move_src (Joint.psd_argument_from_byte x0)
     229
     230(** val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
     231    (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
     232let dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject x2 =
     233  psd_argument_move_src (Joint.dpi1__o__byte_to_hdw_argument x2)
     234
     235(** val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
     236    (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
     237let dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
     238  psd_argument_move_src (Joint.dpi1__o__byte_to_psd_argument x2)
     239
     240(** val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
     241    (Registers.register, 'a1) Types.dPair -> move_src Types.sig0 **)
     242let dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
     243  psd_argument_move_src (Joint.dpi1__o__reg_to_psd_argument x2)
     244
     245(** val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
     246    BitVector.byte Types.sig0 -> move_src Types.sig0 **)
     247let eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject x2 =
     248  psd_argument_move_src (Joint.eject__o__byte_to_hdw_argument x2)
     249
     250(** val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
     251    BitVector.byte Types.sig0 -> move_src Types.sig0 **)
     252let eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
     253  psd_argument_move_src (Joint.eject__o__byte_to_psd_argument x2)
     254
     255(** val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
     256    Registers.register Types.sig0 -> move_src Types.sig0 **)
     257let eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
     258  psd_argument_move_src (Joint.eject__o__reg_to_psd_argument x2)
     259
     260(** val reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
     261    Registers.register -> move_src Types.sig0 **)
     262let reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x0 =
     263  psd_argument_move_src (Joint.psd_argument_from_reg x0)
     264
     265(** val dpi1__o__psd_argument_to_move_src__o__inject :
     266    (Joint.psd_argument, 'a1) Types.dPair -> move_src Types.sig0 **)
     267let dpi1__o__psd_argument_to_move_src__o__inject x2 =
     268  psd_argument_move_src x2.Types.dpi1
     269
     270(** val eject__o__psd_argument_to_move_src__o__inject :
     271    Joint.psd_argument Types.sig0 -> move_src Types.sig0 **)
     272let eject__o__psd_argument_to_move_src__o__inject x2 =
     273  psd_argument_move_src (Types.pi1 x2)
     274
     275(** val psd_argument_to_move_src__o__inject :
     276    Joint.psd_argument -> move_src Types.sig0 **)
     277let psd_argument_to_move_src__o__inject x1 =
     278  psd_argument_move_src x1
     279
     280(** val byte_to_psd_argument__o__psd_argument_to_move_src :
     281    BitVector.byte -> move_src **)
     282let byte_to_psd_argument__o__psd_argument_to_move_src x0 =
     283  psd_argument_move_src (Joint.psd_argument_from_byte x0)
     284
     285(** val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
     286    (BitVector.byte, 'a1) Types.dPair -> move_src **)
     287let dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src x1 =
     288  psd_argument_move_src (Joint.dpi1__o__byte_to_hdw_argument x1)
     289
     290(** val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src :
     291    (BitVector.byte, 'a1) Types.dPair -> move_src **)
     292let dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src x1 =
     293  psd_argument_move_src (Joint.dpi1__o__byte_to_psd_argument x1)
     294
     295(** val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src :
     296    (Registers.register, 'a1) Types.dPair -> move_src **)
     297let dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src x1 =
     298  psd_argument_move_src (Joint.dpi1__o__reg_to_psd_argument x1)
     299
     300(** val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
     301    BitVector.byte Types.sig0 -> move_src **)
     302let eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src x1 =
     303  psd_argument_move_src (Joint.eject__o__byte_to_hdw_argument x1)
     304
     305(** val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src :
     306    BitVector.byte Types.sig0 -> move_src **)
     307let eject__o__byte_to_psd_argument__o__psd_argument_to_move_src x1 =
     308  psd_argument_move_src (Joint.eject__o__byte_to_psd_argument x1)
     309
     310(** val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src :
     311    Registers.register Types.sig0 -> move_src **)
     312let eject__o__reg_to_psd_argument__o__psd_argument_to_move_src x1 =
     313  psd_argument_move_src (Joint.eject__o__reg_to_psd_argument x1)
     314
     315(** val reg_to_psd_argument__o__psd_argument_to_move_src :
     316    Registers.register -> move_src **)
     317let reg_to_psd_argument__o__psd_argument_to_move_src x0 =
     318  psd_argument_move_src (Joint.psd_argument_from_reg x0)
     319
     320(** val dpi1__o__psd_argument_to_move_src :
     321    (Joint.psd_argument, 'a1) Types.dPair -> move_src **)
     322let dpi1__o__psd_argument_to_move_src x1 =
     323  psd_argument_move_src x1.Types.dpi1
     324
     325(** val eject__o__psd_argument_to_move_src :
     326    Joint.psd_argument Types.sig0 -> move_src **)
     327let eject__o__psd_argument_to_move_src x1 =
     328  psd_argument_move_src (Types.pi1 x1)
    201329
    202330type ertl_seq =
     
    210338| Ertl_new_frame -> h_ertl_new_frame
    211339| Ertl_del_frame -> h_ertl_del_frame
    212 | Ertl_frame_size x_212 -> h_ertl_frame_size x_212
     340| Ertl_frame_size x_20966 -> h_ertl_frame_size x_20966
    213341
    214342(** val ertl_seq_rect_Type5 :
     
    217345| Ertl_new_frame -> h_ertl_new_frame
    218346| Ertl_del_frame -> h_ertl_del_frame
    219 | Ertl_frame_size x_217 -> h_ertl_frame_size x_217
     347| Ertl_frame_size x_20971 -> h_ertl_frame_size x_20971
    220348
    221349(** val ertl_seq_rect_Type3 :
     
    224352| Ertl_new_frame -> h_ertl_new_frame
    225353| Ertl_del_frame -> h_ertl_del_frame
    226 | Ertl_frame_size x_222 -> h_ertl_frame_size x_222
     354| Ertl_frame_size x_20976 -> h_ertl_frame_size x_20976
    227355
    228356(** val ertl_seq_rect_Type2 :
     
    231359| Ertl_new_frame -> h_ertl_new_frame
    232360| Ertl_del_frame -> h_ertl_del_frame
    233 | Ertl_frame_size x_227 -> h_ertl_frame_size x_227
     361| Ertl_frame_size x_20981 -> h_ertl_frame_size x_20981
    234362
    235363(** val ertl_seq_rect_Type1 :
     
    238366| Ertl_new_frame -> h_ertl_new_frame
    239367| Ertl_del_frame -> h_ertl_del_frame
    240 | Ertl_frame_size x_232 -> h_ertl_frame_size x_232
     368| Ertl_frame_size x_20986 -> h_ertl_frame_size x_20986
    241369
    242370(** val ertl_seq_rect_Type0 :
     
    245373| Ertl_new_frame -> h_ertl_new_frame
    246374| Ertl_del_frame -> h_ertl_del_frame
    247 | Ertl_frame_size x_237 -> h_ertl_frame_size x_237
     375| Ertl_frame_size x_20991 -> h_ertl_frame_size x_20991
    248376
    249377(** val ertl_seq_inv_rect_Type4 :
     
    304432type ertl_program = Joint.joint_program
    305433
     434(** val dpi1__o__reg_to_ertl_snd_argument__o__inject :
     435    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
     436let dpi1__o__reg_to_ertl_snd_argument__o__inject x2 =
     437  Joint.psd_argument_from_reg x2.Types.dpi1
     438
     439(** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
     440    (Registers.register, 'a1) Types.dPair -> move_src Types.sig0 **)
     441let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
     442  psd_argument_to_move_src__o__inject
     443    (Joint.psd_argument_from_reg x2.Types.dpi1)
     444
     445(** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
     446    (Registers.register, 'a1) Types.dPair -> move_src **)
     447let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
     448  psd_argument_move_src (Joint.psd_argument_from_reg x1.Types.dpi1)
     449
     450(** val eject__o__reg_to_ertl_snd_argument__o__inject :
     451    Registers.register Types.sig0 -> Joint.psd_argument Types.sig0 **)
     452let eject__o__reg_to_ertl_snd_argument__o__inject x2 =
     453  Joint.psd_argument_from_reg (Types.pi1 x2)
     454
     455(** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
     456    Registers.register Types.sig0 -> move_src Types.sig0 **)
     457let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
     458  psd_argument_to_move_src__o__inject
     459    (Joint.psd_argument_from_reg (Types.pi1 x2))
     460
     461(** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
     462    Registers.register Types.sig0 -> move_src **)
     463let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
     464  psd_argument_move_src (Joint.psd_argument_from_reg (Types.pi1 x1))
     465
     466(** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
     467    Registers.register -> move_src **)
     468let reg_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
     469  psd_argument_move_src (Joint.psd_argument_from_reg x0)
     470
     471(** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
     472    Registers.register -> move_src Types.sig0 **)
     473let reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
     474  psd_argument_to_move_src__o__inject (Joint.psd_argument_from_reg x1)
     475
     476(** val reg_to_ertl_snd_argument__o__inject :
     477    Registers.register -> Joint.psd_argument Types.sig0 **)
     478let reg_to_ertl_snd_argument__o__inject x1 =
     479  Joint.psd_argument_from_reg x1
     480
     481(** val dpi1__o__reg_to_ertl_snd_argument :
     482    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument **)
     483let dpi1__o__reg_to_ertl_snd_argument x1 =
     484  Joint.psd_argument_from_reg x1.Types.dpi1
     485
     486(** val eject__o__reg_to_ertl_snd_argument :
     487    Registers.register Types.sig0 -> Joint.psd_argument **)
     488let eject__o__reg_to_ertl_snd_argument x1 =
     489  Joint.psd_argument_from_reg (Types.pi1 x1)
     490
     491(** val dpi1__o__byte_to_ertl_snd_argument__o__inject :
     492    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
     493let dpi1__o__byte_to_ertl_snd_argument__o__inject x2 =
     494  Joint.psd_argument_from_byte x2.Types.dpi1
     495
     496(** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
     497    (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
     498let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
     499  psd_argument_to_move_src__o__inject
     500    (Joint.psd_argument_from_byte x2.Types.dpi1)
     501
     502(** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
     503    (BitVector.byte, 'a1) Types.dPair -> move_src **)
     504let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
     505  psd_argument_move_src (Joint.psd_argument_from_byte x1.Types.dpi1)
     506
     507(** val eject__o__byte_to_ertl_snd_argument__o__inject :
     508    BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0 **)
     509let eject__o__byte_to_ertl_snd_argument__o__inject x2 =
     510  Joint.psd_argument_from_byte (Types.pi1 x2)
     511
     512(** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
     513    BitVector.byte Types.sig0 -> move_src Types.sig0 **)
     514let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
     515  psd_argument_to_move_src__o__inject
     516    (Joint.psd_argument_from_byte (Types.pi1 x2))
     517
     518(** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
     519    BitVector.byte Types.sig0 -> move_src **)
     520let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
     521  psd_argument_move_src (Joint.psd_argument_from_byte (Types.pi1 x1))
     522
     523(** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
     524    BitVector.byte -> move_src **)
     525let byte_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
     526  psd_argument_move_src (Joint.psd_argument_from_byte x0)
     527
     528(** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
     529    BitVector.byte -> move_src Types.sig0 **)
     530let byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
     531  psd_argument_to_move_src__o__inject (Joint.psd_argument_from_byte x1)
     532
     533(** val byte_to_ertl_snd_argument__o__inject :
     534    BitVector.byte -> Joint.psd_argument Types.sig0 **)
     535let byte_to_ertl_snd_argument__o__inject x1 =
     536  Joint.psd_argument_from_byte x1
     537
     538(** val dpi1__o__byte_to_ertl_snd_argument :
     539    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument **)
     540let dpi1__o__byte_to_ertl_snd_argument x1 =
     541  Joint.psd_argument_from_byte x1.Types.dpi1
     542
     543(** val eject__o__byte_to_ertl_snd_argument :
     544    BitVector.byte Types.sig0 -> Joint.psd_argument **)
     545let eject__o__byte_to_ertl_snd_argument x1 =
     546  Joint.psd_argument_from_byte (Types.pi1 x1)
     547
    306548(** val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq **)
    307549let ertl_seq_joint =
    308550  Obj.magic (fun _ x -> Joint.Extension_seq x)
    309551
    310 let byte_to_ertl_snd_argument__o__psd_argument_to_move_src _ = assert false
     552(** val dpi1__o__ertl_seq_to_joint_seq__o__inject :
     553    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
     554    Types.sig0 **)
     555let dpi1__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
     556  ertl_seq_joint x1 x2.Types.dpi1
     557
     558(** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
     559    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
     560    Types.sig0 **)
     561let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
     562  Joint.seq_to_step__o__inject
     563    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTL) x1
     564    (ertl_seq_joint x1 x2.Types.dpi1)
     565
     566(** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
     567    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step **)
     568let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
     569  Joint.Step_seq (ertl_seq_joint x1 x2.Types.dpi1)
     570
     571(** val eject__o__ertl_seq_to_joint_seq__o__inject :
     572    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0 **)
     573let eject__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
     574  ertl_seq_joint x1 (Types.pi1 x2)
     575
     576(** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
     577    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0 **)
     578let eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
     579  Joint.seq_to_step__o__inject
     580    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTL) x1
     581    (ertl_seq_joint x1 (Types.pi1 x2))
     582
     583(** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
     584    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step **)
     585let eject__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
     586  Joint.Step_seq (ertl_seq_joint x1 (Types.pi1 x2))
     587
     588(** val ertl_seq_to_joint_seq__o__seq_to_step :
     589    AST.ident List.list -> __ -> Joint.joint_step **)
     590let ertl_seq_to_joint_seq__o__seq_to_step x0 x1 =
     591  Joint.Step_seq (ertl_seq_joint x0 x1)
     592
     593(** val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
     594    AST.ident List.list -> __ -> Joint.joint_step Types.sig0 **)
     595let ertl_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
     596  Joint.seq_to_step__o__inject
     597    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTL) x0 (ertl_seq_joint x0 x1)
     598
     599(** val ertl_seq_to_joint_seq__o__inject :
     600    AST.ident List.list -> __ -> Joint.joint_seq Types.sig0 **)
     601let ertl_seq_to_joint_seq__o__inject x0 x1 =
     602  ertl_seq_joint x0 x1
     603
     604(** val dpi1__o__ertl_seq_to_joint_seq :
     605    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq **)
     606let dpi1__o__ertl_seq_to_joint_seq x1 x2 =
     607  ertl_seq_joint x1 x2.Types.dpi1
     608
     609(** val eject__o__ertl_seq_to_joint_seq :
     610    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq **)
     611let eject__o__ertl_seq_to_joint_seq x1 x2 =
     612  ertl_seq_joint x1 (Types.pi1 x2)
     613
Note: See TracChangeset for help on using the changeset viewer.