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/globalenvs.mli

    r2730 r2743  
    215215  'a1 genv_t -> Pointers.block -> ('a1, AST.ident) Types.prod Types.option
    216216
     217val opt_eq_from_res__o__ffpi_drop__o__inject :
     218  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     219  Types.sig0
     220
     221val dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject :
     222  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
     223  'a2) Types.dPair -> __ Types.sig0
     224
     225val eject__o__opt_eq_from_res__o__ffpi_drop__o__inject :
     226  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     227  Types.sig0 -> __ Types.sig0
     228
     229val jmeq_to_eq__o__ffpi_drop__o__inject :
     230  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
     231
     232val jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject :
     233  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     234  Types.sig0
     235
     236val dpi1__o__ffpi_drop__o__inject :
     237  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair
     238  -> __ Types.sig0
     239
     240val eject__o__ffpi_drop__o__inject :
     241  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
     242  Types.sig0
     243
     244val ffpi_drop__o__inject :
     245  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
     246
    217247val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident
    218248
     
    221251val find_funct_id :
    222252  'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option
     253
     254val opt_eq_from_res__o__ffi_drop__o__inject :
     255  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     256  Types.sig0
     257
     258val dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject :
     259  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2)
     260  Types.dPair -> __ Types.sig0
     261
     262val eject__o__opt_eq_from_res__o__ffi_drop__o__inject :
     263  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     264  Types.sig0 -> __ Types.sig0
     265
     266val jmeq_to_eq__o__ffi_drop__o__inject :
     267  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
     268
     269val jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject :
     270  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
     271  Types.sig0
     272
     273val dpi1__o__ffi_drop__o__inject :
     274  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair ->
     275  __ Types.sig0
     276
     277val eject__o__ffi_drop__o__inject :
     278  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
     279  Types.sig0
     280
     281val ffi_drop__o__inject :
     282  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
    223283
    224284val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos
Note: See TracChangeset for help on using the changeset viewer.