package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Loc = Serlib.Ser_loc
module CAst = Serlib.Ser_cAst
module Names = Serlib.Ser_names
module Libnames = Serlib.Ser_libnames
val hash_fold_array : 'a Base__Hash.folder -> 'a array Base__Hash.folder
type mutable_flag = bool
val mutable_flag_of_sexp : Sexplib0.Sexp.t -> mutable_flag
val sexp_of_mutable_flag : mutable_flag -> Sexplib0.Sexp.t
val mutable_flag_to_yojson : mutable_flag -> Yojson.Safe.t
val mutable_flag_of_yojson : Yojson.Safe.t -> mutable_flag Ppx_deriving_yojson_runtime.error_or
val hash_fold_mutable_flag : Ppx_hash_lib.Std.Hash.state -> mutable_flag -> Ppx_hash_lib.Std.Hash.state
val hash_mutable_flag : mutable_flag -> Ppx_hash_lib.Std.Hash.hash_value
val compare_mutable_flag : mutable_flag -> mutable_flag -> int
type uid = Names.Id.t
val uid_of_sexp : Sexplib0.Sexp.t -> uid
val sexp_of_uid : uid -> Sexplib0.Sexp.t
val uid_to_yojson : uid -> Yojson.Safe.t
val uid_of_yojson : Yojson.Safe.t -> uid Ppx_deriving_yojson_runtime.error_or
val hash_fold_uid : Ppx_hash_lib.Std.Hash.state -> uid -> Ppx_hash_lib.Std.Hash.state
val hash_uid : uid -> Ppx_hash_lib.Std.Hash.hash_value
val compare_uid : uid -> uid -> int
type lid = Names.Id.t
val lid_of_sexp : Sexplib0.Sexp.t -> lid
val sexp_of_lid : lid -> Sexplib0.Sexp.t
val lid_to_yojson : lid -> Yojson.Safe.t
val lid_of_yojson : Yojson.Safe.t -> lid Ppx_deriving_yojson_runtime.error_or
val hash_fold_lid : Ppx_hash_lib.Std.Hash.state -> lid -> Ppx_hash_lib.Std.Hash.state
val hash_lid : lid -> Ppx_hash_lib.Std.Hash.hash_value
val compare_lid : lid -> lid -> int
type rec_flag = bool
val rec_flag_of_sexp : Sexplib0.Sexp.t -> rec_flag
val sexp_of_rec_flag : rec_flag -> Sexplib0.Sexp.t
val rec_flag_to_yojson : rec_flag -> Yojson.Safe.t
val rec_flag_of_yojson : Yojson.Safe.t -> rec_flag Ppx_deriving_yojson_runtime.error_or
val hash_fold_rec_flag : Ppx_hash_lib.Std.Hash.state -> rec_flag -> Ppx_hash_lib.Std.Hash.state
val hash_rec_flag : rec_flag -> Ppx_hash_lib.Std.Hash.hash_value
val compare_rec_flag : rec_flag -> rec_flag -> int
type redef_flag = bool
val redef_flag_of_sexp : Sexplib0.Sexp.t -> redef_flag
val sexp_of_redef_flag : redef_flag -> Sexplib0.Sexp.t
val redef_flag_to_yojson : redef_flag -> Yojson.Safe.t
val redef_flag_of_yojson : Yojson.Safe.t -> redef_flag Ppx_deriving_yojson_runtime.error_or
val hash_fold_redef_flag : Ppx_hash_lib.Std.Hash.state -> redef_flag -> Ppx_hash_lib.Std.Hash.state
val hash_redef_flag : redef_flag -> Ppx_hash_lib.Std.Hash.hash_value
val compare_redef_flag : redef_flag -> redef_flag -> int
type 'a or_relid = 'a Ltac2_plugin.Tac2expr.or_relid =
  1. | RelId of Libnames.qualid
  2. | AbsKn of 'a
val or_relid_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a or_relid
val sexp_of_or_relid : 'a. ('a -> Sexplib0.Sexp.t) -> 'a or_relid -> Sexplib0.Sexp.t
val or_relid_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a or_relid -> Yojson.Safe.t
val or_relid_of_yojson : 'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a or_relid Ppx_deriving_yojson_runtime.error_or
val hash_fold_or_relid : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a or_relid -> Ppx_hash_lib.Std.Hash.state
val compare_or_relid : 'a. ('a -> 'a -> int) -> 'a or_relid -> 'a or_relid -> int
type 'a or_tuple = 'a Ltac2_plugin.Tac2expr.or_tuple =
  1. | Tuple of int
  2. | Other of 'a
val or_tuple_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a or_tuple
val sexp_of_or_tuple : 'a. ('a -> Sexplib0.Sexp.t) -> 'a or_tuple -> Sexplib0.Sexp.t
val or_tuple_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a or_tuple -> Yojson.Safe.t
val or_tuple_of_yojson : 'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a or_tuple Ppx_deriving_yojson_runtime.error_or
val hash_fold_or_tuple : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a or_tuple -> Ppx_hash_lib.Std.Hash.state
val compare_or_tuple : 'a. ('a -> 'a -> int) -> 'a or_tuple -> 'a or_tuple -> int
type type_constant = Names.KerName.t
val type_constant_of_sexp : Sexplib0.Sexp.t -> type_constant
val sexp_of_type_constant : type_constant -> Sexplib0.Sexp.t
val type_constant_to_yojson : type_constant -> Yojson.Safe.t
val type_constant_of_yojson : Yojson.Safe.t -> type_constant Ppx_deriving_yojson_runtime.error_or
val hash_fold_type_constant : Ppx_hash_lib.Std.Hash.state -> type_constant -> Ppx_hash_lib.Std.Hash.state
val hash_type_constant : type_constant -> Ppx_hash_lib.Std.Hash.hash_value
val compare_type_constant : type_constant -> type_constant -> int
type raw_typexpr_r = Ltac2_plugin.Tac2expr.raw_typexpr_r =
  1. | CTypVar of Names.Name.t
  2. | CTypArrow of raw_typexpr * raw_typexpr
  3. | CTypRef of type_constant or_tuple or_relid * raw_typexpr list
and raw_typexpr = raw_typexpr_r CAst.t
val raw_typexpr_r_of_sexp : Sexplib0__.Sexp.t -> raw_typexpr_r
val raw_typexpr_of_sexp : Sexplib0__.Sexp.t -> raw_typexpr
val sexp_of_raw_typexpr_r : raw_typexpr_r -> Sexplib0__.Sexp.t
val sexp_of_raw_typexpr : raw_typexpr -> Sexplib0__.Sexp.t
val raw_typexpr_r_to_yojson : raw_typexpr_r -> Yojson.Safe.t
val raw_typexpr_r_of_yojson : Yojson.Safe.t -> raw_typexpr_r Ppx_deriving_yojson_runtime.error_or
val raw_typexpr_to_yojson : raw_typexpr -> Yojson.Safe.t
val raw_typexpr_of_yojson : Yojson.Safe.t -> raw_typexpr Ppx_deriving_yojson_runtime.error_or
val hash_fold_raw_typexpr_r : raw_typexpr_r Base__Ppx_hash_lib.hash_fold
val hash_fold_raw_typexpr : raw_typexpr Base__Hash.folder
val hash_raw_typexpr_r : raw_typexpr_r -> Ppx_hash_lib.Std.Hash.hash_value
val hash_raw_typexpr : raw_typexpr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_raw_typexpr_r : raw_typexpr_r -> raw_typexpr_r -> int
val compare_raw_typexpr : raw_typexpr -> raw_typexpr -> int
type raw_typedef = Ltac2_plugin.Tac2expr.raw_typedef =
  1. | CTydDef of raw_typexpr option
  2. | CTydAlg of (uid * raw_typexpr list) list
  3. | CTydRec of (lid * mutable_flag * raw_typexpr) list
  4. | CTydOpn
val raw_typedef_of_sexp : Sexplib0.Sexp.t -> raw_typedef
val sexp_of_raw_typedef : raw_typedef -> Sexplib0.Sexp.t
val raw_typedef_to_yojson : raw_typedef -> Yojson.Safe.t
val raw_typedef_of_yojson : Yojson.Safe.t -> raw_typedef Ppx_deriving_yojson_runtime.error_or
val hash_fold_raw_typedef : Ppx_hash_lib.Std.Hash.state -> raw_typedef -> Ppx_hash_lib.Std.Hash.state
val hash_raw_typedef : raw_typedef -> Ppx_hash_lib.Std.Hash.hash_value
val compare_raw_typedef : raw_typedef -> raw_typedef -> int
type raw_quant_typedef = Names.lident list * raw_typedef
val raw_quant_typedef_of_sexp : Sexplib0.Sexp.t -> raw_quant_typedef
val sexp_of_raw_quant_typedef : raw_quant_typedef -> Sexplib0.Sexp.t
val raw_quant_typedef_to_yojson : raw_quant_typedef -> Yojson.Safe.t
val raw_quant_typedef_of_yojson : Yojson.Safe.t -> raw_quant_typedef Ppx_deriving_yojson_runtime.error_or
val hash_fold_raw_quant_typedef : Ppx_hash_lib.Std.Hash.state -> raw_quant_typedef -> Ppx_hash_lib.Std.Hash.state
val hash_raw_quant_typedef : raw_quant_typedef -> Ppx_hash_lib.Std.Hash.hash_value
val compare_raw_quant_typedef : raw_quant_typedef -> raw_quant_typedef -> int
type atom = Ltac2_plugin.Tac2expr.atom =
  1. | AtmInt of int
  2. | AtmStr of string
val atom_of_sexp : Sexplib0.Sexp.t -> atom
val sexp_of_atom : atom -> Sexplib0.Sexp.t
val atom_to_yojson : atom -> Yojson.Safe.t
val atom_of_yojson : Yojson.Safe.t -> atom Ppx_deriving_yojson_runtime.error_or
val hash_fold_atom : Ppx_hash_lib.Std.Hash.state -> atom -> Ppx_hash_lib.Std.Hash.state
val hash_atom : atom -> Ppx_hash_lib.Std.Hash.hash_value
val compare_atom : atom -> atom -> int
type ltac_constant = Names.KerName.t
val ltac_constant_of_sexp : Sexplib0.Sexp.t -> ltac_constant
val sexp_of_ltac_constant : ltac_constant -> Sexplib0.Sexp.t
val ltac_constant_to_yojson : ltac_constant -> Yojson.Safe.t
val ltac_constant_of_yojson : Yojson.Safe.t -> ltac_constant Ppx_deriving_yojson_runtime.error_or
val hash_fold_ltac_constant : Ppx_hash_lib.Std.Hash.state -> ltac_constant -> Ppx_hash_lib.Std.Hash.state
val hash_ltac_constant : ltac_constant -> Ppx_hash_lib.Std.Hash.hash_value
val compare_ltac_constant : ltac_constant -> ltac_constant -> int
type ltac_alias = Names.KerName.t
val ltac_alias_of_sexp : Sexplib0.Sexp.t -> ltac_alias
val sexp_of_ltac_alias : ltac_alias -> Sexplib0.Sexp.t
val ltac_alias_to_yojson : ltac_alias -> Yojson.Safe.t
val ltac_alias_of_yojson : Yojson.Safe.t -> ltac_alias Ppx_deriving_yojson_runtime.error_or
val hash_fold_ltac_alias : Ppx_hash_lib.Std.Hash.state -> ltac_alias -> Ppx_hash_lib.Std.Hash.state
val hash_ltac_alias : ltac_alias -> Ppx_hash_lib.Std.Hash.hash_value
val compare_ltac_alias : ltac_alias -> ltac_alias -> int
type ltac_constructor = Names.KerName.t
val ltac_constructor_of_sexp : Sexplib0.Sexp.t -> ltac_constructor
val sexp_of_ltac_constructor : ltac_constructor -> Sexplib0.Sexp.t
val ltac_constructor_to_yojson : ltac_constructor -> Yojson.Safe.t
val ltac_constructor_of_yojson : Yojson.Safe.t -> ltac_constructor Ppx_deriving_yojson_runtime.error_or
val hash_fold_ltac_constructor : Ppx_hash_lib.Std.Hash.state -> ltac_constructor -> Ppx_hash_lib.Std.Hash.state
val hash_ltac_constructor : ltac_constructor -> Ppx_hash_lib.Std.Hash.hash_value
val compare_ltac_constructor : ltac_constructor -> ltac_constructor -> int
type ltac_projection = Names.KerName.t
val ltac_projection_of_sexp : Sexplib0.Sexp.t -> ltac_projection
val sexp_of_ltac_projection : ltac_projection -> Sexplib0.Sexp.t
val ltac_projection_to_yojson : ltac_projection -> Yojson.Safe.t
val ltac_projection_of_yojson : Yojson.Safe.t -> ltac_projection Ppx_deriving_yojson_runtime.error_or
val hash_fold_ltac_projection : Ppx_hash_lib.Std.Hash.state -> ltac_projection -> Ppx_hash_lib.Std.Hash.state
val hash_ltac_projection : ltac_projection -> Ppx_hash_lib.Std.Hash.hash_value
val compare_ltac_projection : ltac_projection -> ltac_projection -> int
type raw_patexpr = raw_patexpr_r CAst.t
and raw_patexpr_r = Ltac2_plugin.Tac2expr.raw_patexpr_r =
  1. | CPatVar of Names.Name.t
  2. | CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
  3. | CPatCnv of raw_patexpr * raw_typexpr
val raw_patexpr_of_sexp : Sexplib0__.Sexp.t -> raw_patexpr
val raw_patexpr_r_of_sexp : Sexplib0__.Sexp.t -> raw_patexpr_r
val sexp_of_raw_patexpr : raw_patexpr -> Sexplib0__.Sexp.t
val sexp_of_raw_patexpr_r : raw_patexpr_r -> Sexplib0__.Sexp.t
val raw_patexpr_to_yojson : raw_patexpr -> Yojson.Safe.t
val raw_patexpr_of_yojson : Yojson.Safe.t -> raw_patexpr Ppx_deriving_yojson_runtime.error_or
val raw_patexpr_r_to_yojson : raw_patexpr_r -> Yojson.Safe.t
val raw_patexpr_r_of_yojson : Yojson.Safe.t -> raw_patexpr_r Ppx_deriving_yojson_runtime.error_or
val hash_fold_raw_patexpr : raw_patexpr Base__Hash.folder
val hash_fold_raw_patexpr_r : raw_patexpr_r Base__Ppx_hash_lib.hash_fold
val hash_raw_patexpr : raw_patexpr -> Ppx_hash_lib.Std.Hash.hash_value
val hash_raw_patexpr_r : raw_patexpr_r -> Ppx_hash_lib.Std.Hash.hash_value
val compare_raw_patexpr : raw_patexpr -> raw_patexpr -> int
val compare_raw_patexpr_r : raw_patexpr_r -> raw_patexpr_r -> int
type tacref = Ltac2_plugin.Tac2expr.tacref =
  1. | TacConstant of ltac_constant
  2. | TacAlias of ltac_alias
val tacref_of_sexp : Sexplib0.Sexp.t -> tacref
val sexp_of_tacref : tacref -> Sexplib0.Sexp.t
val tacref_to_yojson : tacref -> Yojson.Safe.t
val tacref_of_yojson : Yojson.Safe.t -> tacref Ppx_deriving_yojson_runtime.error_or
val hash_fold_tacref : Ppx_hash_lib.Std.Hash.state -> tacref -> Ppx_hash_lib.Std.Hash.state
val hash_tacref : tacref -> Ppx_hash_lib.Std.Hash.hash_value
val compare_tacref : tacref -> tacref -> int
module ObjS : sig ... end
module Obj : sig ... end
module T2ESpec : sig ... end
module T2E : sig ... end
type raw_tacexpr_r = T2E.t
val raw_tacexpr_r_of_sexp : Sexplib0.Sexp.t -> raw_tacexpr_r
val sexp_of_raw_tacexpr_r : raw_tacexpr_r -> Sexplib0.Sexp.t
val raw_tacexpr_r_to_yojson : raw_tacexpr_r -> Yojson.Safe.t
val raw_tacexpr_r_of_yojson : Yojson.Safe.t -> raw_tacexpr_r Ppx_deriving_yojson_runtime.error_or
val hash_fold_raw_tacexpr_r : Ppx_hash_lib.Std.Hash.state -> raw_tacexpr_r -> Ppx_hash_lib.Std.Hash.state
val hash_raw_tacexpr_r : raw_tacexpr_r -> Ppx_hash_lib.Std.Hash.hash_value
val compare_raw_tacexpr_r : raw_tacexpr_r -> raw_tacexpr_r -> int
type raw_tacexpr = raw_tacexpr_r CAst.t
val raw_tacexpr_of_sexp : Sexplib0.Sexp.t -> raw_tacexpr
val sexp_of_raw_tacexpr : raw_tacexpr -> Sexplib0.Sexp.t
val raw_tacexpr_to_yojson : raw_tacexpr -> Yojson.Safe.t
val raw_tacexpr_of_yojson : Yojson.Safe.t -> raw_tacexpr Ppx_deriving_yojson_runtime.error_or
val hash_fold_raw_tacexpr : Ppx_hash_lib.Std.Hash.state -> raw_tacexpr -> Ppx_hash_lib.Std.Hash.state
val hash_raw_tacexpr : raw_tacexpr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_raw_tacexpr : raw_tacexpr -> raw_tacexpr -> int
type ml_tactic_name = Ltac2_plugin.Tac2expr.ml_tactic_name = {
  1. mltac_plugin : string;
  2. mltac_tactic : string;
}
val ml_tactic_name_of_sexp : Sexplib0.Sexp.t -> ml_tactic_name
val sexp_of_ml_tactic_name : ml_tactic_name -> Sexplib0.Sexp.t
val ml_tactic_name_to_yojson : ml_tactic_name -> Yojson.Safe.t
val ml_tactic_name_of_yojson : Yojson.Safe.t -> ml_tactic_name Ppx_deriving_yojson_runtime.error_or
val hash_fold_ml_tactic_name : Ppx_hash_lib.Std.Hash.state -> ml_tactic_name -> Ppx_hash_lib.Std.Hash.state
val hash_ml_tactic_name : ml_tactic_name -> Ppx_hash_lib.Std.Hash.hash_value
val compare_ml_tactic_name : ml_tactic_name -> ml_tactic_name -> int
type sexpr = Ltac2_plugin.Tac2expr.sexpr =
  1. | SexprStr of string CAst.t
  2. | SexprInt of int CAst.t
  3. | SexprRec of Loc.t * Names.Id.t option CAst.t * sexpr list
val sexpr_of_sexp : Sexplib0__.Sexp.t -> sexpr
val sexp_of_sexpr : sexpr -> Sexplib0__.Sexp.t
val sexpr_to_yojson : sexpr -> Yojson.Safe.t
val sexpr_of_yojson : Yojson.Safe.t -> sexpr Ppx_deriving_yojson_runtime.error_or
val hash_fold_sexpr : sexpr Base__Hash.folder
val hash_sexpr : sexpr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_sexpr : sexpr -> sexpr -> int
type strexpr = Ltac2_plugin.Tac2expr.strexpr =
  1. | StrVal of mutable_flag * rec_flag * (Names.lname * raw_tacexpr) list
  2. | StrTyp of rec_flag * (Libnames.qualid * redef_flag * raw_quant_typedef) list
  3. | StrPrm of Names.lident * raw_typexpr * ml_tactic_name
  4. | StrSyn of sexpr list * int option * raw_tacexpr
  5. | StrMut of Libnames.qualid * Names.lident option * raw_tacexpr
val strexpr_of_sexp : Sexplib0.Sexp.t -> strexpr
val sexp_of_strexpr : strexpr -> Sexplib0.Sexp.t
val strexpr_to_yojson : strexpr -> Yojson.Safe.t
val strexpr_of_yojson : Yojson.Safe.t -> strexpr Ppx_deriving_yojson_runtime.error_or
val hash_fold_strexpr : Ppx_hash_lib.Std.Hash.state -> strexpr -> Ppx_hash_lib.Std.Hash.state
val hash_strexpr : strexpr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_strexpr : strexpr -> strexpr -> int
type case_info = type_constant or_tuple
val case_info_of_sexp : Sexplib0.Sexp.t -> case_info
val sexp_of_case_info : case_info -> Sexplib0.Sexp.t
val case_info_to_yojson : case_info -> Yojson.Safe.t
val case_info_of_yojson : Yojson.Safe.t -> case_info Ppx_deriving_yojson_runtime.error_or
val hash_fold_case_info : Ppx_hash_lib.Std.Hash.state -> case_info -> Ppx_hash_lib.Std.Hash.state
val hash_case_info : case_info -> Ppx_hash_lib.Std.Hash.hash_value
val compare_case_info : case_info -> case_info -> int
type 'a open_match = 'a Ltac2_plugin.Tac2expr.open_match = {
  1. opn_match : 'a;
  2. opn_branch : (Names.Name.t * Names.Name.t array * 'a) Names.KNmap.t;
  3. opn_default : Names.Name.t * 'a;
}
val open_match_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a open_match
val sexp_of_open_match : 'a. ('a -> Sexplib0.Sexp.t) -> 'a open_match -> Sexplib0.Sexp.t
val open_match_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a open_match -> Yojson.Safe.t
val open_match_of_yojson : 'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a open_match Ppx_deriving_yojson_runtime.error_or
val hash_fold_open_match : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a open_match -> Ppx_hash_lib.Std.Hash.state
val compare_open_match : 'a. ('a -> 'a -> int) -> 'a open_match -> 'a open_match -> int
module GT2ESpec : sig ... end
module GT2E : sig ... end
type glb_tacexpr = GT2E.t
val glb_tacexpr_of_sexp : Sexplib0.Sexp.t -> glb_tacexpr
val sexp_of_glb_tacexpr : glb_tacexpr -> Sexplib0.Sexp.t
val glb_tacexpr_to_yojson : glb_tacexpr -> Yojson.Safe.t
val glb_tacexpr_of_yojson : Yojson.Safe.t -> glb_tacexpr Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> glb_tacexpr Ppx_deriving_yojson_runtime.error_or
val hash_fold_glb_tacexpr : Ppx_hash_lib.Std.Hash.state -> glb_tacexpr -> Ppx_hash_lib.Std.Hash.state
val hash_glb_tacexpr : glb_tacexpr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_glb_tacexpr : glb_tacexpr -> glb_tacexpr -> int
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