package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.18.0.0.18.3.tbz
sha256=d9a32c0033d720032011e9bf5e8d30d4b205ce276b6a81ab359fc461809e9b63
sha512=742d2b92b986e45044c19cd2bbfd5dd5346cfb4b0ec20f40811d8b0096c6e25192528359f98d2eed2a74ae67790d1f8cea382cb01fd7cf8903a5a917cca79a84

doc/serlib_ltac2/Serlib_ltac2/Ser_tac2expr/index.html

Module Serlib_ltac2.Ser_tac2exprSource

module Loc = Serlib.Ser_loc
module CAst = Serlib.Ser_cAst
module Names = Serlib.Ser_names
module Libnames = Serlib.Ser_libnames
Sourceval hash_fold_array : 'a Base__Hash.folder -> 'a array Base__Hash.folder
Sourcetype mutable_flag = bool
Sourceval mutable_flag_of_sexp : Sexplib0.Sexp.t -> mutable_flag
Sourceval sexp_of_mutable_flag : mutable_flag -> Sexplib0.Sexp.t
Sourceval mutable_flag_to_yojson : mutable_flag -> Yojson.Safe.t
Sourceval mutable_flag_of_yojson : Yojson.Safe.t -> mutable_flag Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_mutable_flag : Ppx_hash_lib.Std.Hash.state -> mutable_flag -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_mutable_flag : mutable_flag -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_mutable_flag : mutable_flag -> mutable_flag -> int
Sourcetype uid = Names.Id.t
Sourceval uid_of_sexp : Sexplib0.Sexp.t -> uid
Sourceval sexp_of_uid : uid -> Sexplib0.Sexp.t
Sourceval uid_to_yojson : uid -> Yojson.Safe.t
Sourceval uid_of_yojson : Yojson.Safe.t -> uid Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_uid : Ppx_hash_lib.Std.Hash.state -> uid -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_uid : uid -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_uid : uid -> uid -> int
Sourcetype lid = Names.Id.t
Sourceval lid_of_sexp : Sexplib0.Sexp.t -> lid
Sourceval sexp_of_lid : lid -> Sexplib0.Sexp.t
Sourceval lid_to_yojson : lid -> Yojson.Safe.t
Sourceval lid_of_yojson : Yojson.Safe.t -> lid Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_lid : Ppx_hash_lib.Std.Hash.state -> lid -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_lid : lid -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_lid : lid -> lid -> int
Sourcetype rec_flag = bool
Sourceval rec_flag_of_sexp : Sexplib0.Sexp.t -> rec_flag
Sourceval sexp_of_rec_flag : rec_flag -> Sexplib0.Sexp.t
Sourceval rec_flag_to_yojson : rec_flag -> Yojson.Safe.t
Sourceval rec_flag_of_yojson : Yojson.Safe.t -> rec_flag Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_rec_flag : Ppx_hash_lib.Std.Hash.state -> rec_flag -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_rec_flag : rec_flag -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_rec_flag : rec_flag -> rec_flag -> int
Sourcetype redef_flag = bool
Sourceval redef_flag_of_sexp : Sexplib0.Sexp.t -> redef_flag
Sourceval sexp_of_redef_flag : redef_flag -> Sexplib0.Sexp.t
Sourceval redef_flag_to_yojson : redef_flag -> Yojson.Safe.t
Sourceval redef_flag_of_yojson : Yojson.Safe.t -> redef_flag Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_redef_flag : Ppx_hash_lib.Std.Hash.state -> redef_flag -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_redef_flag : redef_flag -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_redef_flag : redef_flag -> redef_flag -> int
Sourcetype 'a or_relid = 'a Ltac2_plugin.Tac2expr.or_relid =
  1. | RelId of Libnames.qualid
  2. | AbsKn of 'a
Sourceval or_relid_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a or_relid
Sourceval sexp_of_or_relid : 'a. ('a -> Sexplib0.Sexp.t) -> 'a or_relid -> Sexplib0.Sexp.t
Sourceval or_relid_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a or_relid -> Yojson.Safe.t
Sourceval 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
Sourceval 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
Sourceval compare_or_relid : 'a. ('a -> 'a -> int) -> 'a or_relid -> 'a or_relid -> int
Sourcetype 'a or_tuple = 'a Ltac2_plugin.Tac2expr.or_tuple =
  1. | Tuple of int
  2. | Other of 'a
Sourceval or_tuple_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a or_tuple
Sourceval sexp_of_or_tuple : 'a. ('a -> Sexplib0.Sexp.t) -> 'a or_tuple -> Sexplib0.Sexp.t
Sourceval or_tuple_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a or_tuple -> Yojson.Safe.t
Sourceval 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
Sourceval 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
Sourceval compare_or_tuple : 'a. ('a -> 'a -> int) -> 'a or_tuple -> 'a or_tuple -> int
Sourcetype type_constant = Names.KerName.t
Sourceval type_constant_of_sexp : Sexplib0.Sexp.t -> type_constant
Sourceval sexp_of_type_constant : type_constant -> Sexplib0.Sexp.t
Sourceval type_constant_to_yojson : type_constant -> Yojson.Safe.t
Sourceval type_constant_of_yojson : Yojson.Safe.t -> type_constant Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_type_constant : Ppx_hash_lib.Std.Hash.state -> type_constant -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_type_constant : type_constant -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_type_constant : type_constant -> type_constant -> int
Sourcetype 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
Sourceand raw_typexpr = raw_typexpr_r CAst.t
Sourceval raw_typexpr_r_of_sexp : Sexplib0__.Sexp.t -> raw_typexpr_r
Sourceval raw_typexpr_of_sexp : Sexplib0__.Sexp.t -> raw_typexpr
Sourceval sexp_of_raw_typexpr_r : raw_typexpr_r -> Sexplib0__.Sexp.t
Sourceval sexp_of_raw_typexpr : raw_typexpr -> Sexplib0__.Sexp.t
Sourceval raw_typexpr_r_to_yojson : raw_typexpr_r -> Yojson.Safe.t
Sourceval raw_typexpr_r_of_yojson : Yojson.Safe.t -> raw_typexpr_r Ppx_deriving_yojson_runtime.error_or
Sourceval raw_typexpr_to_yojson : raw_typexpr -> Yojson.Safe.t
Sourceval raw_typexpr_of_yojson : Yojson.Safe.t -> raw_typexpr Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_raw_typexpr_r : raw_typexpr_r Base__Ppx_hash_lib.hash_fold
Sourceval hash_fold_raw_typexpr : raw_typexpr Base__Hash.folder
Sourceval hash_raw_typexpr_r : raw_typexpr_r -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_raw_typexpr : raw_typexpr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_raw_typexpr_r : raw_typexpr_r -> raw_typexpr_r -> int
Sourceval compare_raw_typexpr : raw_typexpr -> raw_typexpr -> int
Sourcetype 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
Sourceval raw_typedef_of_sexp : Sexplib0.Sexp.t -> raw_typedef
Sourceval sexp_of_raw_typedef : raw_typedef -> Sexplib0.Sexp.t
Sourceval raw_typedef_to_yojson : raw_typedef -> Yojson.Safe.t
Sourceval raw_typedef_of_yojson : Yojson.Safe.t -> raw_typedef Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_raw_typedef : Ppx_hash_lib.Std.Hash.state -> raw_typedef -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_raw_typedef : raw_typedef -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_raw_typedef : raw_typedef -> raw_typedef -> int
Sourcetype raw_quant_typedef = Names.lident list * raw_typedef
Sourceval raw_quant_typedef_of_sexp : Sexplib0.Sexp.t -> raw_quant_typedef
Sourceval sexp_of_raw_quant_typedef : raw_quant_typedef -> Sexplib0.Sexp.t
Sourceval raw_quant_typedef_to_yojson : raw_quant_typedef -> Yojson.Safe.t
Sourceval raw_quant_typedef_of_yojson : Yojson.Safe.t -> raw_quant_typedef Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_raw_quant_typedef : Ppx_hash_lib.Std.Hash.state -> raw_quant_typedef -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_raw_quant_typedef : raw_quant_typedef -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_raw_quant_typedef : raw_quant_typedef -> raw_quant_typedef -> int
Sourcetype atom = Ltac2_plugin.Tac2expr.atom =
  1. | AtmInt of int
  2. | AtmStr of string
Sourceval atom_of_sexp : Sexplib0.Sexp.t -> atom
Sourceval sexp_of_atom : atom -> Sexplib0.Sexp.t
Sourceval atom_to_yojson : atom -> Yojson.Safe.t
Sourceval atom_of_yojson : Yojson.Safe.t -> atom Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_atom : Ppx_hash_lib.Std.Hash.state -> atom -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_atom : atom -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_atom : atom -> atom -> int
Sourcetype ltac_constant = Names.KerName.t
Sourceval ltac_constant_of_sexp : Sexplib0.Sexp.t -> ltac_constant
Sourceval sexp_of_ltac_constant : ltac_constant -> Sexplib0.Sexp.t
Sourceval ltac_constant_to_yojson : ltac_constant -> Yojson.Safe.t
Sourceval ltac_constant_of_yojson : Yojson.Safe.t -> ltac_constant Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ltac_constant : Ppx_hash_lib.Std.Hash.state -> ltac_constant -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ltac_constant : ltac_constant -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ltac_constant : ltac_constant -> ltac_constant -> int
Sourcetype ltac_alias = Names.KerName.t
Sourceval ltac_alias_of_sexp : Sexplib0.Sexp.t -> ltac_alias
Sourceval sexp_of_ltac_alias : ltac_alias -> Sexplib0.Sexp.t
Sourceval ltac_alias_to_yojson : ltac_alias -> Yojson.Safe.t
Sourceval ltac_alias_of_yojson : Yojson.Safe.t -> ltac_alias Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ltac_alias : Ppx_hash_lib.Std.Hash.state -> ltac_alias -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ltac_alias : ltac_alias -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ltac_alias : ltac_alias -> ltac_alias -> int
Sourcetype ltac_constructor = Names.KerName.t
Sourceval ltac_constructor_of_sexp : Sexplib0.Sexp.t -> ltac_constructor
Sourceval sexp_of_ltac_constructor : ltac_constructor -> Sexplib0.Sexp.t
Sourceval ltac_constructor_to_yojson : ltac_constructor -> Yojson.Safe.t
Sourceval ltac_constructor_of_yojson : Yojson.Safe.t -> ltac_constructor Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ltac_constructor : Ppx_hash_lib.Std.Hash.state -> ltac_constructor -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ltac_constructor : ltac_constructor -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ltac_constructor : ltac_constructor -> ltac_constructor -> int
Sourcetype ltac_projection = Names.KerName.t
Sourceval ltac_projection_of_sexp : Sexplib0.Sexp.t -> ltac_projection
Sourceval sexp_of_ltac_projection : ltac_projection -> Sexplib0.Sexp.t
Sourceval ltac_projection_to_yojson : ltac_projection -> Yojson.Safe.t
Sourceval ltac_projection_of_yojson : Yojson.Safe.t -> ltac_projection Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ltac_projection : Ppx_hash_lib.Std.Hash.state -> ltac_projection -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ltac_projection : ltac_projection -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ltac_projection : ltac_projection -> ltac_projection -> int
Sourcetype raw_patexpr = raw_patexpr_r CAst.t
Sourceand raw_patexpr_r = Ltac2_plugin.Tac2expr.raw_patexpr_r =
  1. | CPatVar of Names.Name.t
  2. | CPatAtm of atom
  3. | CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
  4. | CPatRecord of (ltac_projection or_relid * raw_patexpr) list
  5. | CPatCnv of raw_patexpr * raw_typexpr
  6. | CPatOr of raw_patexpr list
  7. | CPatAs of raw_patexpr * Names.lident
Sourceval raw_patexpr_of_sexp : Sexplib0__.Sexp.t -> raw_patexpr
Sourceval raw_patexpr_r_of_sexp : Sexplib0__.Sexp.t -> raw_patexpr_r
Sourceval sexp_of_raw_patexpr : raw_patexpr -> Sexplib0__.Sexp.t
Sourceval sexp_of_raw_patexpr_r : raw_patexpr_r -> Sexplib0__.Sexp.t
Sourceval raw_patexpr_to_yojson : raw_patexpr -> Yojson.Safe.t
Sourceval raw_patexpr_of_yojson : Yojson.Safe.t -> raw_patexpr Ppx_deriving_yojson_runtime.error_or
Sourceval raw_patexpr_r_to_yojson : raw_patexpr_r -> Yojson.Safe.t
Sourceval raw_patexpr_r_of_yojson : Yojson.Safe.t -> raw_patexpr_r Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_raw_patexpr : raw_patexpr Base__Hash.folder
Sourceval hash_fold_raw_patexpr_r : raw_patexpr_r Base__Ppx_hash_lib.hash_fold
Sourceval hash_raw_patexpr : raw_patexpr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_raw_patexpr_r : raw_patexpr_r -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_raw_patexpr : raw_patexpr -> raw_patexpr -> int
Sourceval compare_raw_patexpr_r : raw_patexpr_r -> raw_patexpr_r -> int
Sourcetype tacref = Ltac2_plugin.Tac2expr.tacref =
  1. | TacConstant of ltac_constant
  2. | TacAlias of ltac_alias
Sourceval tacref_of_sexp : Sexplib0.Sexp.t -> tacref
Sourceval sexp_of_tacref : tacref -> Sexplib0.Sexp.t
Sourceval tacref_to_yojson : tacref -> Yojson.Safe.t
Sourceval tacref_of_yojson : Yojson.Safe.t -> tacref Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_tacref : Ppx_hash_lib.Std.Hash.state -> tacref -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_tacref : tacref -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_tacref : tacref -> tacref -> int
Sourcemodule ObjS : sig ... end
module Obj : sig ... end
Sourcemodule T2ESpec : sig ... end
module T2E : sig ... end
Sourcetype raw_tacexpr_r = T2E.t
Sourceval raw_tacexpr_r_of_sexp : Sexplib0.Sexp.t -> raw_tacexpr_r
Sourceval sexp_of_raw_tacexpr_r : raw_tacexpr_r -> Sexplib0.Sexp.t
Sourceval raw_tacexpr_r_to_yojson : raw_tacexpr_r -> Yojson.Safe.t
Sourceval raw_tacexpr_r_of_yojson : Yojson.Safe.t -> raw_tacexpr_r Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_raw_tacexpr_r : Ppx_hash_lib.Std.Hash.state -> raw_tacexpr_r -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_raw_tacexpr_r : raw_tacexpr_r -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_raw_tacexpr_r : raw_tacexpr_r -> raw_tacexpr_r -> int
Sourcetype raw_tacexpr = raw_tacexpr_r CAst.t
Sourceval raw_tacexpr_of_sexp : Sexplib0.Sexp.t -> raw_tacexpr
Sourceval sexp_of_raw_tacexpr : raw_tacexpr -> Sexplib0.Sexp.t
Sourceval raw_tacexpr_to_yojson : raw_tacexpr -> Yojson.Safe.t
Sourceval raw_tacexpr_of_yojson : Yojson.Safe.t -> raw_tacexpr Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_raw_tacexpr : Ppx_hash_lib.Std.Hash.state -> raw_tacexpr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_raw_tacexpr : raw_tacexpr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_raw_tacexpr : raw_tacexpr -> raw_tacexpr -> int
Sourcetype ml_tactic_name = Ltac2_plugin.Tac2expr.ml_tactic_name = {
  1. mltac_plugin : string;
  2. mltac_tactic : string;
}
Sourceval ml_tactic_name_of_sexp : Sexplib0.Sexp.t -> ml_tactic_name
Sourceval sexp_of_ml_tactic_name : ml_tactic_name -> Sexplib0.Sexp.t
Sourceval ml_tactic_name_to_yojson : ml_tactic_name -> Yojson.Safe.t
Sourceval ml_tactic_name_of_yojson : Yojson.Safe.t -> ml_tactic_name Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ml_tactic_name : Ppx_hash_lib.Std.Hash.state -> ml_tactic_name -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ml_tactic_name : ml_tactic_name -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ml_tactic_name : ml_tactic_name -> ml_tactic_name -> int
Sourcetype 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
Sourceval sexpr_of_sexp : Sexplib0__.Sexp.t -> sexpr
Sourceval sexp_of_sexpr : sexpr -> Sexplib0__.Sexp.t
Sourceval sexpr_to_yojson : sexpr -> Yojson.Safe.t
Sourceval sexpr_of_yojson : Yojson.Safe.t -> sexpr Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_sexpr : sexpr Base__Hash.folder
Sourceval hash_sexpr : sexpr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_sexpr : sexpr -> sexpr -> int
Sourcetype 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. | StrMut of Libnames.qualid * Names.lident option * raw_tacexpr
Sourceval strexpr_of_sexp : Sexplib0.Sexp.t -> strexpr
Sourceval sexp_of_strexpr : strexpr -> Sexplib0.Sexp.t
Sourceval strexpr_to_yojson : strexpr -> Yojson.Safe.t
Sourceval strexpr_of_yojson : Yojson.Safe.t -> strexpr Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_strexpr : Ppx_hash_lib.Std.Hash.state -> strexpr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_strexpr : strexpr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_strexpr : strexpr -> strexpr -> int
Sourcetype ctor_indx = Ltac2_plugin.Tac2expr.ctor_indx =
  1. | Closed of int
  2. | Open of ltac_constructor
Sourceval ctor_indx_of_sexp : Sexplib0.Sexp.t -> ctor_indx
Sourceval sexp_of_ctor_indx : ctor_indx -> Sexplib0.Sexp.t
Sourceval ctor_indx_to_yojson : ctor_indx -> Yojson.Safe.t
Sourceval ctor_indx_of_yojson : Yojson.Safe.t -> ctor_indx Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ctor_indx : Ppx_hash_lib.Std.Hash.state -> ctor_indx -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ctor_indx : ctor_indx -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ctor_indx : ctor_indx -> ctor_indx -> int
Sourcetype ctor_data_for_patterns = Ltac2_plugin.Tac2expr.ctor_data_for_patterns = {
  1. ctyp : type_constant option;
  2. cnargs : int;
  3. cindx : ctor_indx;
}
Sourceval ctor_data_for_patterns_of_sexp : Sexplib0.Sexp.t -> ctor_data_for_patterns
Sourceval sexp_of_ctor_data_for_patterns : ctor_data_for_patterns -> Sexplib0.Sexp.t
Sourceval ctor_data_for_patterns_to_yojson : ctor_data_for_patterns -> Yojson.Safe.t
Sourceval ctor_data_for_patterns_of_yojson : Yojson.Safe.t -> ctor_data_for_patterns Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ctor_data_for_patterns : Ppx_hash_lib.Std.Hash.state -> ctor_data_for_patterns -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ctor_data_for_patterns : ctor_data_for_patterns -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ctor_data_for_patterns : ctor_data_for_patterns -> ctor_data_for_patterns -> int
Sourcetype glb_pat = Ltac2_plugin.Tac2expr.glb_pat =
  1. | GPatVar of Names.Name.t
  2. | GPatAtm of atom
  3. | GPatRef of ctor_data_for_patterns * glb_pat list
  4. | GPatOr of glb_pat list
  5. | GPatAs of glb_pat * Names.Id.t
Sourceval glb_pat_of_sexp : Sexplib0__.Sexp.t -> glb_pat
Sourceval sexp_of_glb_pat : glb_pat -> Sexplib0__.Sexp.t
Sourceval glb_pat_to_yojson : glb_pat -> Yojson.Safe.t
Sourceval glb_pat_of_yojson : Yojson.Safe.t -> glb_pat Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_glb_pat : glb_pat Base__Hash.folder
Sourceval hash_glb_pat : glb_pat -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_glb_pat : glb_pat -> glb_pat -> int
Sourcetype case_info = type_constant or_tuple
Sourceval case_info_of_sexp : Sexplib0.Sexp.t -> case_info
Sourceval sexp_of_case_info : case_info -> Sexplib0.Sexp.t
Sourceval case_info_to_yojson : case_info -> Yojson.Safe.t
Sourceval case_info_of_yojson : Yojson.Safe.t -> case_info Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_case_info : Ppx_hash_lib.Std.Hash.state -> case_info -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_case_info : case_info -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_case_info : case_info -> case_info -> int
Sourcetype '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;
}
Sourceval open_match_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a open_match
Sourceval sexp_of_open_match : 'a. ('a -> Sexplib0.Sexp.t) -> 'a open_match -> Sexplib0.Sexp.t
Sourceval open_match_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a open_match -> Yojson.Safe.t
Sourceval 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
Sourceval 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
Sourceval compare_open_match : 'a. ('a -> 'a -> int) -> 'a open_match -> 'a open_match -> int
Sourcemodule GT2ESpec : sig ... end
module GT2E : sig ... end
Sourcetype glb_tacexpr = GT2E.t
Sourceval glb_tacexpr_of_sexp : Sexplib0.Sexp.t -> glb_tacexpr
Sourceval sexp_of_glb_tacexpr : glb_tacexpr -> Sexplib0.Sexp.t
Sourceval glb_tacexpr_to_yojson : glb_tacexpr -> Yojson.Safe.t
Sourceval glb_tacexpr_of_yojson : Yojson.Safe.t -> glb_tacexpr Ppx_deriving_yojson_runtime.error_or
Sourceval _ : Yojson.Safe.t -> glb_tacexpr Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_glb_tacexpr : Ppx_hash_lib.Std.Hash.state -> glb_tacexpr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_glb_tacexpr : glb_tacexpr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_glb_tacexpr : glb_tacexpr -> glb_tacexpr -> int