package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type retroknowledge
type entry = Constr.t
type int31_field =
  1. | Int31Bits
  2. | Int31Type
  3. | Int31Constructor
  4. | Int31Twice
  5. | Int31TwicePlusOne
  6. | Int31Phi
  7. | Int31PhiInv
  8. | Int31Plus
  9. | Int31PlusC
  10. | Int31PlusCarryC
  11. | Int31Minus
  12. | Int31MinusC
  13. | Int31MinusCarryC
  14. | Int31Times
  15. | Int31TimesC
  16. | Int31Div21
  17. | Int31Div
  18. | Int31Diveucl
  19. | Int31AddMulDiv
  20. | Int31Compare
  21. | Int31Head0
  22. | Int31Tail0
  23. | Int31Lor
  24. | Int31Land
  25. | Int31Lxor
type field =
  1. | KInt31 of string * int31_field
type action =
  1. | RKRegister of field * entry
val initial_retroknowledge : retroknowledge
val get_vm_compiling_info : retroknowledge -> entry -> Cinstr.lambda array -> Cinstr.lambda
val get_vm_constant_static_info : retroknowledge -> entry -> Constr.constr array -> Cinstr.lambda
val get_vm_constant_dynamic_info : retroknowledge -> entry -> Cinstr.lambda array -> Cinstr.lambda
val get_vm_before_match_info : retroknowledge -> entry -> Cinstr.lambda -> Cinstr.lambda
val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> Constr.constr
val get_native_compiling_info : retroknowledge -> entry -> Nativeinstr.prefix -> Nativeinstr.lambda array -> Nativeinstr.lambda
val get_native_constant_static_info : retroknowledge -> entry -> Constr.constr array -> Nativeinstr.lambda
val get_native_constant_dynamic_info : retroknowledge -> entry -> Nativeinstr.prefix -> Names.constructor -> Nativeinstr.lambda array -> Nativeinstr.lambda
val add_field : retroknowledge -> field -> entry -> retroknowledge
val mem : retroknowledge -> field -> bool
val find : retroknowledge -> field -> entry
type reactive_info = {
  1. vm_compiling : (bool -> Cinstr.lambda array -> Cinstr.lambda) option;
  2. vm_constant_static : (bool -> Constr.constr array -> Cinstr.lambda) option;
  3. vm_constant_dynamic : (bool -> Cinstr.lambda array -> Cinstr.lambda) option;
  4. vm_before_match : (bool -> Cinstr.lambda -> Cinstr.lambda) option;
  5. vm_decompile_const : (int -> Constr.constr) option;
  6. native_compiling : (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array -> Nativeinstr.lambda) option;
  7. native_constant_static : (bool -> Constr.constr array -> Nativeinstr.lambda) option;
  8. native_constant_dynamic : (bool -> Nativeinstr.prefix -> Names.constructor -> Nativeinstr.lambda array -> Nativeinstr.lambda) option;
  9. native_before_match : (bool -> Nativeinstr.prefix -> Names.constructor -> Nativeinstr.lambda -> Nativeinstr.lambda) option;
}
val empty_reactive_info : reactive_info
val dispatch_hook : (retroknowledge -> entry -> field -> reactive_info) Hook.t