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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct