package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install

Dune Dependency

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

Authors

  1. E
    Emilio Jesús Gallego Arias <e@x80.org>
  2. A
    Ali Caglayan <alizter@gmail.com>
  3. S
    Shachar Itzhaky <shachari@cs.technion.ac.il>
  4. R
    Ramkumar Ramachandra <r@artagnon.com>

Maintainers

  1. E
    e@x80.org

Sources

coq-lsp-0.2.3.9.0.tbz
sha256=8776582dddfe768623870cf540ff6ba1e96a44a36e85db18ab93d238d640f92a
sha512=2837889bf99bfe715bd0e752782211a76a14aac71ed37a4fb784f4f0abe338352c9c6d8caa37daf79c036997add1cb306c523f793625b38709f3b5e245380223

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
module Attributes = Serlib.Ser_attributes
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 (Attributes.vernac_flags * 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 'a glb_typexpr = 'a Ltac2_plugin.Tac2expr.glb_typexpr =
  1. | GTypVar of 'a
  2. | GTypArrow of 'a glb_typexpr * 'a glb_typexpr
  3. | GTypRef of type_constant or_tuple * 'a glb_typexpr list
Sourceval glb_typexpr_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a glb_typexpr
Sourceval sexp_of_glb_typexpr : 'a. ('a -> Sexplib0.Sexp.t) -> 'a glb_typexpr -> Sexplib0.Sexp.t
Sourceval glb_typexpr_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a glb_typexpr -> Yojson.Safe.t
Sourceval glb_typexpr_of_yojson : 'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a glb_typexpr Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_glb_typexpr : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a glb_typexpr -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_glb_typexpr : 'a. ('a -> 'a -> int) -> 'a glb_typexpr -> 'a glb_typexpr -> 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
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 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 ObjS : sig ... end
module Obj : sig ... end
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 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
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 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 _ : 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
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