package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
module CAst = Serlib.Ser_cAst
module Libnames = Serlib.Ser_libnames
module Constrexpr = Serlib.Ser_constrexpr
module Tactypes = Serlib.Ser_tactypes
module Genintern = Serlib.Ser_genintern
module EConstr = Serlib.Ser_eConstr
module Tacexpr = Serlib_ltac.Ser_tacexpr
module Ltac_plugin : sig ... end
type 'constr coeff_spec = 'constr Ring_plugin.Ring_ast.coeff_spec =
  1. | Computational of 'constr
  2. | Abstract
  3. | Morphism of 'constr
val coeff_spec_of_sexp : 'constr. (Sexplib0.Sexp.t -> 'constr) -> Sexplib0.Sexp.t -> 'constr coeff_spec
val sexp_of_coeff_spec : 'constr. ('constr -> Sexplib0.Sexp.t) -> 'constr coeff_spec -> Sexplib0.Sexp.t
val hash_fold_coeff_spec : 'constr. (Ppx_hash_lib.Std.Hash.state -> 'constr -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'constr coeff_spec -> Ppx_hash_lib.Std.Hash.state
val compare_coeff_spec : 'constr. ('constr -> 'constr -> int) -> 'constr coeff_spec -> 'constr coeff_spec -> int
type cst_tac_spec = Ring_plugin.Ring_ast.cst_tac_spec =
  1. | CstTac of Ltac_plugin.Tacexpr.raw_tactic_expr
  2. | Closed of Libnames.qualid list
val cst_tac_spec_of_sexp : Sexplib0.Sexp.t -> cst_tac_spec
val sexp_of_cst_tac_spec : cst_tac_spec -> Sexplib0.Sexp.t
val hash_fold_cst_tac_spec : Ppx_hash_lib.Std.Hash.state -> cst_tac_spec -> Ppx_hash_lib.Std.Hash.state
val hash_cst_tac_spec : cst_tac_spec -> Ppx_hash_lib.Std.Hash.hash_value
val compare_cst_tac_spec : cst_tac_spec -> cst_tac_spec -> int
type 'constr ring_mod = 'constr Ring_plugin.Ring_ast.ring_mod =
  1. | Ring_kind of 'constr coeff_spec
  2. | Const_tac of cst_tac_spec
  3. | Pre_tac of Ltac_plugin.Tacexpr.raw_tactic_expr
  4. | Post_tac of Ltac_plugin.Tacexpr.raw_tactic_expr
  5. | Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr
  6. | Pow_spec of cst_tac_spec * Constrexpr.constr_expr
  7. | Sign_spec of Constrexpr.constr_expr
  8. | Div_spec of Constrexpr.constr_expr
val ring_mod_of_sexp : 'constr. (Sexplib0.Sexp.t -> 'constr) -> Sexplib0.Sexp.t -> 'constr ring_mod
val sexp_of_ring_mod : 'constr. ('constr -> Sexplib0.Sexp.t) -> 'constr ring_mod -> Sexplib0.Sexp.t
val hash_fold_ring_mod : 'constr. (Ppx_hash_lib.Std.Hash.state -> 'constr -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'constr ring_mod -> Ppx_hash_lib.Std.Hash.state
val compare_ring_mod : 'constr. ('constr -> 'constr -> int) -> 'constr ring_mod -> 'constr ring_mod -> int
type 'a field_mod = 'a Ring_plugin.Ring_ast.field_mod =
  1. | Ring_mod of 'a ring_mod
  2. | Inject of Constrexpr.constr_expr
val field_mod_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a field_mod
val sexp_of_field_mod : 'a. ('a -> Sexplib0.Sexp.t) -> 'a field_mod -> Sexplib0.Sexp.t
val hash_fold_field_mod : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a field_mod -> Ppx_hash_lib.Std.Hash.state
val compare_field_mod : 'a. ('a -> 'a -> int) -> 'a field_mod -> 'a field_mod -> int
module A0 : sig ... end
val ser_wit_field_mod : (A0.t, Util.Empty.t, Util.Empty.t) Serlib__Ser_genarg.gen_ser
module A1 : sig ... end
val ser_wit_field_mods : (A1.t, Util.Empty.t, Util.Empty.t) Serlib__Ser_genarg.gen_ser
module A2 : sig ... end
val ser_wit_ring_mod : (A2.t, Util.Empty.t, Util.Empty.t) Serlib__Ser_genarg.gen_ser
module A3 : sig ... end
val ser_wit_ring_mods : (A3.t, Util.Empty.t, Util.Empty.t) Serlib__Ser_genarg.gen_ser
val register : unit -> unit
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