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
type mutable_flag = bool
val mutable_flag_to_yojson : mutable_flag -> Yojson.Safe.t
val mutable_flag_of_sexp : Sexplib0.Sexp.t -> mutable_flag
val sexp_of_mutable_flag : mutable_flag -> Sexplib0.Sexp.t
val hash_fold_mutable_flag : Base.Hash.state -> mutable_flag -> Base.Hash.state
val hash_mutable_flag : mutable_flag -> Base.Hash.hash_value
val compare_mutable_flag : mutable_flag -> mutable_flag -> int
type uid = Names.Id.t
val uid_to_yojson : uid -> Yojson.Safe.t
val uid_of_sexp : Sexplib0.Sexp.t -> uid
val sexp_of_uid : uid -> Sexplib0.Sexp.t
val hash_fold_uid : Base.Hash.state -> uid -> Base.Hash.state
val hash_uid : uid -> Base.Hash.hash_value
val compare_uid : uid -> uid -> int
type lid = Names.Id.t
val lid_to_yojson : lid -> Yojson.Safe.t
val lid_of_sexp : Sexplib0.Sexp.t -> lid
val sexp_of_lid : lid -> Sexplib0.Sexp.t
val hash_fold_lid : Base.Hash.state -> lid -> Base.Hash.state
val hash_lid : lid -> Base.Hash.hash_value
val compare_lid : lid -> lid -> int
type rec_flag = bool
val rec_flag_to_yojson : rec_flag -> Yojson.Safe.t
val rec_flag_of_sexp : Sexplib0.Sexp.t -> rec_flag
val sexp_of_rec_flag : rec_flag -> Sexplib0.Sexp.t
val hash_fold_rec_flag : Base.Hash.state -> rec_flag -> Base.Hash.state
val hash_rec_flag : rec_flag -> Base.Hash.hash_value
val compare_rec_flag : rec_flag -> rec_flag -> int
type redef_flag = bool
val redef_flag_to_yojson : redef_flag -> Yojson.Safe.t
val redef_flag_of_sexp : Sexplib0.Sexp.t -> redef_flag
val sexp_of_redef_flag : redef_flag -> Sexplib0.Sexp.t
val hash_fold_redef_flag : Base.Hash.state -> redef_flag -> Base.Hash.state
val hash_redef_flag : redef_flag -> Base.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_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a or_relid -> Yojson.Safe.t
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 hash_fold_or_relid : 'a. (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a or_relid -> Base.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_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a or_tuple -> Yojson.Safe.t
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 hash_fold_or_tuple : 'a. (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a or_tuple -> Base.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_to_yojson : type_constant -> Yojson.Safe.t
val type_constant_of_sexp : Sexplib0.Sexp.t -> type_constant
val sexp_of_type_constant : type_constant -> Sexplib0.Sexp.t
val hash_fold_type_constant : Base.Hash.state -> type_constant -> Base.Hash.state
val hash_type_constant : type_constant -> Base.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_to_yojson : raw_typexpr_r -> Yojson.Safe.t
val raw_typexpr_to_yojson : raw_typexpr -> Yojson.Safe.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 hash_fold_raw_typexpr_r : Base.Hash.state -> raw_typexpr_r -> Base.Hash.state
val hash_raw_typexpr_r : raw_typexpr_r -> Base.Hash.hash_value
val hash_raw_typexpr : raw_typexpr -> Base.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_to_yojson : raw_typedef -> Yojson.Safe.t
val raw_typedef_of_sexp : Sexplib0.Sexp.t -> raw_typedef
val sexp_of_raw_typedef : raw_typedef -> Sexplib0.Sexp.t
val hash_fold_raw_typedef : Base.Hash.state -> raw_typedef -> Base.Hash.state
val hash_raw_typedef : raw_typedef -> Base.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_to_yojson : raw_quant_typedef -> Yojson.Safe.t
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 hash_fold_raw_quant_typedef : Base.Hash.state -> raw_quant_typedef -> Base.Hash.state
val hash_raw_quant_typedef : raw_quant_typedef -> Base.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_to_yojson : atom -> Yojson.Safe.t
val atom_of_sexp : Sexplib0.Sexp.t -> atom
val sexp_of_atom : atom -> Sexplib0.Sexp.t
val hash_fold_atom : Base.Hash.state -> atom -> Base.Hash.state
val hash_atom : atom -> Base.Hash.hash_value
val compare_atom : atom -> atom -> int
type ltac_constant = Names.KerName.t
val ltac_constant_to_yojson : ltac_constant -> Yojson.Safe.t
val ltac_constant_of_sexp : Sexplib0.Sexp.t -> ltac_constant
val sexp_of_ltac_constant : ltac_constant -> Sexplib0.Sexp.t
val hash_fold_ltac_constant : Base.Hash.state -> ltac_constant -> Base.Hash.state
val hash_ltac_constant : ltac_constant -> Base.Hash.hash_value
val compare_ltac_constant : ltac_constant -> ltac_constant -> int
type ltac_alias = Names.KerName.t
val ltac_alias_to_yojson : ltac_alias -> Yojson.Safe.t
val ltac_alias_of_sexp : Sexplib0.Sexp.t -> ltac_alias
val sexp_of_ltac_alias : ltac_alias -> Sexplib0.Sexp.t
val hash_fold_ltac_alias : Base.Hash.state -> ltac_alias -> Base.Hash.state
val hash_ltac_alias : ltac_alias -> Base.Hash.hash_value
val compare_ltac_alias : ltac_alias -> ltac_alias -> int
type ltac_constructor = Names.KerName.t
val ltac_constructor_to_yojson : ltac_constructor -> Yojson.Safe.t
val ltac_constructor_of_sexp : Sexplib0.Sexp.t -> ltac_constructor
val sexp_of_ltac_constructor : ltac_constructor -> Sexplib0.Sexp.t
val hash_fold_ltac_constructor : Base.Hash.state -> ltac_constructor -> Base.Hash.state
val hash_ltac_constructor : ltac_constructor -> Base.Hash.hash_value
val compare_ltac_constructor : ltac_constructor -> ltac_constructor -> int
type ltac_projection = Names.KerName.t
val ltac_projection_to_yojson : ltac_projection -> Yojson.Safe.t
val ltac_projection_of_sexp : Sexplib0.Sexp.t -> ltac_projection
val sexp_of_ltac_projection : ltac_projection -> Sexplib0.Sexp.t
val hash_fold_ltac_projection : Base.Hash.state -> ltac_projection -> Base.Hash.state
val hash_ltac_projection : ltac_projection -> Base.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_to_yojson : raw_patexpr -> Yojson.Safe.t
val raw_patexpr_r_to_yojson : raw_patexpr_r -> Yojson.Safe.t
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 hash_fold_raw_patexpr_r : Base.Hash.state -> raw_patexpr_r -> Base.Hash.state
val hash_raw_patexpr : raw_patexpr -> Base.Hash.hash_value
val hash_raw_patexpr_r : raw_patexpr_r -> Base.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_to_yojson : tacref -> Yojson.Safe.t
val tacref_of_sexp : Sexplib0.Sexp.t -> tacref
val sexp_of_tacref : tacref -> Sexplib0.Sexp.t
val hash_fold_tacref : Base.Hash.state -> tacref -> Base.Hash.state
val hash_tacref : tacref -> Base.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_to_yojson : raw_tacexpr_r -> Yojson.Safe.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 hash_fold_raw_tacexpr_r : Base.Hash.state -> raw_tacexpr_r -> Base.Hash.state
val hash_raw_tacexpr_r : raw_tacexpr_r -> Base.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_to_yojson : raw_tacexpr -> Yojson.Safe.t
val raw_tacexpr_of_sexp : Sexplib0.Sexp.t -> raw_tacexpr
val sexp_of_raw_tacexpr : raw_tacexpr -> Sexplib0.Sexp.t
val hash_fold_raw_tacexpr : Base.Hash.state -> raw_tacexpr -> Base.Hash.state
val hash_raw_tacexpr : raw_tacexpr -> Base.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_to_yojson : ml_tactic_name -> Yojson.Safe.t
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 hash_fold_ml_tactic_name : Base.Hash.state -> ml_tactic_name -> Base.Hash.state
val hash_ml_tactic_name : ml_tactic_name -> Base.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_to_yojson : sexpr -> Yojson.Safe.t
val sexpr_of_sexp : Sexplib0.Sexp.t -> sexpr
val sexp_of_sexpr : sexpr -> Sexplib0.Sexp.t
val hash_sexpr : sexpr -> Base.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_to_yojson : strexpr -> Yojson.Safe.t
val strexpr_of_sexp : Sexplib0.Sexp.t -> strexpr
val sexp_of_strexpr : strexpr -> Sexplib0.Sexp.t
val hash_fold_strexpr : Base.Hash.state -> strexpr -> Base.Hash.state
val hash_strexpr : strexpr -> Base.Hash.hash_value
val compare_strexpr : strexpr -> strexpr -> int
type case_info = type_constant or_tuple
val case_info_to_yojson : case_info -> Yojson.Safe.t
val case_info_of_sexp : Sexplib0.Sexp.t -> case_info
val sexp_of_case_info : case_info -> Sexplib0.Sexp.t
val hash_fold_case_info : Base.Hash.state -> case_info -> Base.Hash.state
val hash_case_info : case_info -> Base.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_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a open_match -> Yojson.Safe.t
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 hash_fold_open_match : 'a. (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a open_match -> Base.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_to_yojson : glb_tacexpr -> Yojson.Safe.t
val _ : Yojson.Safe.t -> glb_tacexpr Ppx_deriving_yojson_runtime.error_or
val glb_tacexpr_of_sexp : Sexplib0.Sexp.t -> glb_tacexpr
val sexp_of_glb_tacexpr : glb_tacexpr -> Sexplib0.Sexp.t
val hash_fold_glb_tacexpr : Base.Hash.state -> glb_tacexpr -> Base.Hash.state
val hash_glb_tacexpr : glb_tacexpr -> Base.Hash.hash_value
val compare_glb_tacexpr : glb_tacexpr -> glb_tacexpr -> int