package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Genintern = Serlib.Ser_genintern
module Geninterp = Serlib.Ser_geninterp
type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind =
  1. | InParens
  2. | WithAt
  3. | NoFlag
  4. | Cpattern
val ssrtermkind_to_yojson : ssrtermkind -> Yojson.Safe.t
val ssrtermkind_of_yojson : Yojson.Safe.t -> ssrtermkind Ppx_deriving_yojson_runtime.error_or
val ssrtermkind_of_sexp : Sexplib0.Sexp.t -> ssrtermkind
val sexp_of_ssrtermkind : ssrtermkind -> Sexplib0.Sexp.t
val hash_fold_ssrtermkind : Base.Hash.state -> ssrtermkind -> Base.Hash.state
val hash_ssrtermkind : ssrtermkind -> Base.Hash.hash_value
val compare_ssrtermkind : ssrtermkind -> ssrtermkind -> int
type cpattern = Ssrmatching_plugin.Ssrmatching.cpattern = {
  1. kind : ssrtermkind;
  2. pattern : Genintern.glob_constr_and_expr;
  3. interpretation : Geninterp.interp_sign option;
}
val cpattern_to_yojson : cpattern -> Yojson.Safe.t
val cpattern_of_yojson : Yojson.Safe.t -> cpattern Ppx_deriving_yojson_runtime.error_or
val cpattern_of_sexp : Sexplib0.Sexp.t -> cpattern
val sexp_of_cpattern : cpattern -> Sexplib0.Sexp.t
val hash_fold_cpattern : Base.Hash.state -> cpattern -> Base.Hash.state
val hash_cpattern : cpattern -> Base.Hash.hash_value
val compare_cpattern : cpattern -> cpattern -> int
type ('a, 'b) ssrpattern = ('a, 'b) Ssrmatching_plugin.Ssrmatching.ssrpattern =
  1. | T of 'b
  2. | In_T of 'b
  3. | X_In_T of 'a * 'b
  4. | In_X_In_T of 'a * 'b
  5. | E_In_X_In_T of 'b * 'a * 'b
  6. | E_As_X_In_T of 'b * 'a * 'b
val ssrpattern_to_yojson : 'a 'b. ('a -> Yojson.Safe.t) -> ('b -> Yojson.Safe.t) -> ('a, 'b) ssrpattern -> Yojson.Safe.t
val ssrpattern_of_yojson : 'a 'b. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> (Yojson.Safe.t -> 'b Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> ('a, 'b) ssrpattern Ppx_deriving_yojson_runtime.error_or
val ssrpattern_of_sexp : 'a 'b. (Sexplib0.Sexp.t -> 'a) -> (Sexplib0.Sexp.t -> 'b) -> Sexplib0.Sexp.t -> ('a, 'b) ssrpattern
val sexp_of_ssrpattern : 'a 'b. ('a -> Sexplib0.Sexp.t) -> ('b -> Sexplib0.Sexp.t) -> ('a, 'b) ssrpattern -> Sexplib0.Sexp.t
val hash_fold_ssrpattern : 'a 'b. (Base.Hash.state -> 'a -> Base.Hash.state) -> (Base.Hash.state -> 'b -> Base.Hash.state) -> Base.Hash.state -> ('a, 'b) ssrpattern -> Base.Hash.state
val compare_ssrpattern : 'a 'b. ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a, 'b) ssrpattern -> ('a, 'b) ssrpattern -> int
module PierceRPattern : sig ... end
module B_ : sig ... end
type rpattern = B_.t
val rpattern_to_yojson : rpattern -> Yojson.Safe.t
val rpattern_of_yojson : Yojson.Safe.t -> rpattern Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> rpattern Ppx_deriving_yojson_runtime.error_or
val rpattern_of_sexp : Sexplib0.Sexp.t -> rpattern
val sexp_of_rpattern : rpattern -> Sexplib0.Sexp.t
val hash_fold_rpattern : Base.Hash.state -> rpattern -> Base.Hash.state
val hash_rpattern : rpattern -> Base.Hash.hash_value
val compare_rpattern : rpattern -> rpattern -> int
type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir =
  1. | L2R
  2. | R2L
val ssrdir_of_sexp : Sexplib0.Sexp.t -> ssrdir
val sexp_of_ssrdir : ssrdir -> Sexplib0.Sexp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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