package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
type direction_flag = bool
val direction_flag_of_sexp : Sexplib.Sexp.t -> direction_flag
val sexp_of_direction_flag : direction_flag -> Sexplib.Sexp.t
type lazy_flag = Ltac_plugin.Tacexpr.lazy_flag =
  1. | General
  2. | Select
  3. | Once
val lazy_flag_of_sexp : Sexplib.Sexp.t -> lazy_flag
val sexp_of_lazy_flag : lazy_flag -> Sexplib.Sexp.t
type global_flag = Ltac_plugin.Tacexpr.global_flag =
  1. | TacGlobal
  2. | TacLocal
val global_flag_of_sexp : Sexplib.Sexp.t -> global_flag
val sexp_of_global_flag : global_flag -> Sexplib.Sexp.t
type evars_flag = bool
val evars_flag_of_sexp : Sexplib.Sexp.t -> evars_flag
val sexp_of_evars_flag : evars_flag -> Sexplib.Sexp.t
type rec_flag = bool
val rec_flag_of_sexp : Sexplib.Sexp.t -> rec_flag
val sexp_of_rec_flag : rec_flag -> Sexplib.Sexp.t
type advanced_flag = bool
val advanced_flag_of_sexp : Sexplib.Sexp.t -> advanced_flag
val sexp_of_advanced_flag : advanced_flag -> Sexplib.Sexp.t
type letin_flag = bool
val letin_flag_of_sexp : Sexplib.Sexp.t -> letin_flag
val sexp_of_letin_flag : letin_flag -> Sexplib.Sexp.t
type clear_flag = bool option
val clear_flag_of_sexp : Sexplib.Sexp.t -> clear_flag
val sexp_of_clear_flag : clear_flag -> Sexplib.Sexp.t
type ('c, 'd, 'id) inversion_strength = ('c, 'd, 'id) Ltac_plugin.Tacexpr.inversion_strength
val inversion_strength_of_sexp : (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> ('c, 'd, 'id) inversion_strength
val sexp_of_inversion_strength : ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('id -> Sexplib.Sexp.t) -> ('c, 'd, 'id) inversion_strength -> Sexplib.Sexp.t
type ('a, 'b) location = ('a, 'b) Ltac_plugin.Tacexpr.location =
  1. | HypLocation of 'a
  2. | ConclLocation of 'b
val sexp_of_location : ('a -> Sexplib0.Sexp.t) -> ('b -> Sexplib0.Sexp.t) -> ('a, 'b) location -> Sexplib0.Sexp.t
val location_of_sexp : (Sexplib0.Sexp.t -> 'a) -> (Sexplib0.Sexp.t -> 'b) -> Sexplib0.Sexp.t -> ('a, 'b) location
val hash_fold_location : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> (Ppx_hash_lib.Std.Hash.state -> 'b -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> ('a, 'b) location -> Ppx_hash_lib.Std.Hash.state
val compare_location : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a, 'b) location -> ('a, 'b) location -> int
type 'id message_token = 'id Ltac_plugin.Tacexpr.message_token
val message_token_of_sexp : (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> 'id message_token
val sexp_of_message_token : ('id -> Sexplib.Sexp.t) -> 'id message_token -> Sexplib.Sexp.t
type ('dconstr, 'id) induction_clause = ('dconstr, 'id) Ltac_plugin.Tacexpr.induction_clause
val induction_clause_of_sexp : (Sexplib.Sexp.t -> 'dconstr) -> (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> ('dconstr, 'id) induction_clause
val sexp_of_induction_clause : ('dconstr -> Sexplib.Sexp.t) -> ('id -> Sexplib.Sexp.t) -> ('dconstr, 'id) induction_clause -> Sexplib.Sexp.t
type ('constr, 'dconstr, 'id) induction_clause_list = ('constr, 'dconstr, 'id) Ltac_plugin.Tacexpr.induction_clause_list
val induction_clause_list_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'dconstr) -> (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> ('constr, 'dconstr, 'id) induction_clause_list
val sexp_of_induction_clause_list : ('constr -> Sexplib.Sexp.t) -> ('dconstr -> Sexplib.Sexp.t) -> ('id -> Sexplib.Sexp.t) -> ('constr, 'dconstr, 'id) induction_clause_list -> Sexplib.Sexp.t
type 'a with_bindings_arg = 'a Ltac_plugin.Tacexpr.with_bindings_arg
val with_bindings_arg_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a with_bindings_arg
val sexp_of_with_bindings_arg : ('a -> Sexplib.Sexp.t) -> 'a with_bindings_arg -> Sexplib.Sexp.t
type 'a match_pattern = 'a Ltac_plugin.Tacexpr.match_pattern
val match_pattern_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a match_pattern
val sexp_of_match_pattern : ('a -> Sexplib.Sexp.t) -> 'a match_pattern -> Sexplib.Sexp.t
type 'a match_context_hyps = 'a Ltac_plugin.Tacexpr.match_context_hyps
val match_context_hyps_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a match_context_hyps
val sexp_of_match_context_hyps : ('a -> Sexplib.Sexp.t) -> 'a match_context_hyps -> Sexplib.Sexp.t
type ('a, 't) match_rule = ('a, 't) Ltac_plugin.Tacexpr.match_rule
val match_rule_of_sexp : (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 't) -> Sexplib.Sexp.t -> ('a, 't) match_rule
val sexp_of_match_rule : ('a -> Sexplib.Sexp.t) -> ('t -> Sexplib.Sexp.t) -> ('a, 't) match_rule -> Sexplib.Sexp.t
val ml_tactic_name_of_sexp : Sexplib.Sexp.t -> ml_tactic_name
val sexp_of_ml_tactic_name : ml_tactic_name -> Sexplib.Sexp.t
type 'd gen_atomic_tactic_expr = 'd Ltac_plugin.Tacexpr.gen_atomic_tactic_expr
val sexp_of_gen_atomic_tactic_expr : ('a -> Sexplib.Sexp.t) -> ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('e -> Sexplib.Sexp.t) -> ('f -> Sexplib.Sexp.t) -> ('g -> Sexplib.Sexp.t) -> ('h -> Sexplib.Sexp.t) -> ('i -> Sexplib.Sexp.t) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_atomic_tactic_expr -> Sexplib.Sexp.t
val sexp_of_gen_tactic_expr : ('a -> Sexplib.Sexp.t) -> ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('e -> Sexplib.Sexp.t) -> ('f -> Sexplib.Sexp.t) -> ('g -> Sexplib.Sexp.t) -> ('h -> Sexplib.Sexp.t) -> ('i -> Sexplib.Sexp.t) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_expr -> Sexplib.Sexp.t
val sexp_of_gen_tactic_arg : ('a -> Sexplib.Sexp.t) -> ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('e -> Sexplib.Sexp.t) -> ('f -> Sexplib.Sexp.t) -> ('g -> Sexplib.Sexp.t) -> ('h -> Sexplib.Sexp.t) -> ('i -> Sexplib.Sexp.t) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_arg -> Sexplib.Sexp.t
val sexp_of_gen_fun_ast : ('a -> Sexplib.Sexp.t) -> ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('e -> Sexplib.Sexp.t) -> ('f -> Sexplib.Sexp.t) -> ('g -> Sexplib.Sexp.t) -> ('h -> Sexplib.Sexp.t) -> ('i -> Sexplib.Sexp.t) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_fun_ast -> Sexplib.Sexp.t
val gen_atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'e) -> (Sexplib.Sexp.t -> 'f) -> (Sexplib.Sexp.t -> 'g) -> (Sexplib.Sexp.t -> 'h) -> (Sexplib.Sexp.t -> 'i) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_atomic_tactic_expr
val gen_tactic_expr_of_sexp : Sexplib.Sexp.t -> (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'e) -> (Sexplib.Sexp.t -> 'f) -> (Sexplib.Sexp.t -> 'g) -> (Sexplib.Sexp.t -> 'h) -> (Sexplib.Sexp.t -> 'i) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_expr
val gen_tactic_arg_of_sexp : Sexplib.Sexp.t -> (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'e) -> (Sexplib.Sexp.t -> 'f) -> (Sexplib.Sexp.t -> 'g) -> (Sexplib.Sexp.t -> 'h) -> (Sexplib.Sexp.t -> 'i) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_arg
val gen_fun_ast_of_sexp : Sexplib.Sexp.t -> (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'e) -> (Sexplib.Sexp.t -> 'f) -> (Sexplib.Sexp.t -> 'g) -> (Sexplib.Sexp.t -> 'h) -> (Sexplib.Sexp.t -> 'i) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_fun_ast
type glob_tactic_expr = Ltac_plugin.Tacexpr.glob_tactic_expr
val sexp_of_glob_tactic_expr : glob_tactic_expr -> Sexplib0.Sexp.t
val glob_tactic_expr_of_sexp : Sexplib0.Sexp.t -> glob_tactic_expr
val glob_tactic_expr_to_yojson : glob_tactic_expr -> Yojson.Safe.t
val glob_tactic_expr_of_yojson : Yojson.Safe.t -> glob_tactic_expr Ppx_deriving_yojson_runtime.error_or
val hash_fold_glob_tactic_expr : Ppx_hash_lib.Std.Hash.state -> glob_tactic_expr -> Ppx_hash_lib.Std.Hash.state
val hash_glob_tactic_expr : glob_tactic_expr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_glob_tactic_expr : glob_tactic_expr -> glob_tactic_expr -> int
type glob_atomic_tactic_expr = Ltac_plugin.Tacexpr.glob_atomic_tactic_expr
val sexp_of_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> Sexplib0.Sexp.t
val glob_atomic_tactic_expr_of_sexp : Sexplib0.Sexp.t -> glob_atomic_tactic_expr
val glob_atomic_tactic_expr_to_yojson : glob_atomic_tactic_expr -> Yojson.Safe.t
val glob_atomic_tactic_expr_of_yojson : Yojson.Safe.t -> glob_atomic_tactic_expr Ppx_deriving_yojson_runtime.error_or
val hash_fold_glob_atomic_tactic_expr : Ppx_hash_lib.Std.Hash.state -> glob_atomic_tactic_expr -> Ppx_hash_lib.Std.Hash.state
val hash_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> glob_atomic_tactic_expr -> int
val sexp_of_raw_tactic_expr : raw_tactic_expr -> Sexplib0.Sexp.t
val raw_tactic_expr_of_sexp : Sexplib0.Sexp.t -> raw_tactic_expr
val raw_tactic_expr_to_yojson : raw_tactic_expr -> Yojson.Safe.t
val raw_tactic_expr_of_yojson : Yojson.Safe.t -> raw_tactic_expr Ppx_deriving_yojson_runtime.error_or
val hash_fold_raw_tactic_expr : Ppx_hash_lib.Std.Hash.state -> raw_tactic_expr -> Ppx_hash_lib.Std.Hash.state
val hash_raw_tactic_expr : raw_tactic_expr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_raw_tactic_expr : raw_tactic_expr -> raw_tactic_expr -> int
type raw_atomic_tactic_expr = Ltac_plugin.Tacexpr.raw_atomic_tactic_expr
val sexp_of_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> Sexplib0.Sexp.t
val raw_atomic_tactic_expr_of_sexp : Sexplib0.Sexp.t -> raw_atomic_tactic_expr
val raw_atomic_tactic_expr_to_yojson : raw_atomic_tactic_expr -> Yojson.Safe.t
val raw_atomic_tactic_expr_of_yojson : Yojson.Safe.t -> raw_atomic_tactic_expr Ppx_deriving_yojson_runtime.error_or
val hash_fold_raw_atomic_tactic_expr : Ppx_hash_lib.Std.Hash.state -> raw_atomic_tactic_expr -> Ppx_hash_lib.Std.Hash.state
val hash_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> raw_atomic_tactic_expr -> int
type atomic_tactic_expr = Ltac_plugin.Tacexpr.atomic_tactic_expr
val atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> atomic_tactic_expr
val sexp_of_atomic_tactic_expr : atomic_tactic_expr -> Sexplib.Sexp.t
type tacdef_body = Ltac_plugin.Tacexpr.tacdef_body
val sexp_of_tacdef_body : tacdef_body -> Sexplib0.Sexp.t
val tacdef_body_of_sexp : Sexplib0.Sexp.t -> tacdef_body
val hash_fold_tacdef_body : Ppx_hash_lib.Std.Hash.state -> tacdef_body -> Ppx_hash_lib.Std.Hash.state
val hash_tacdef_body : tacdef_body -> Ppx_hash_lib.Std.Hash.hash_value
val compare_tacdef_body : tacdef_body -> tacdef_body -> int
val sexp_of_intro_pattern : intro_pattern -> Sexplib0.Sexp.t
val intro_pattern_of_sexp : Sexplib0.Sexp.t -> intro_pattern
val hash_fold_intro_pattern : Ppx_hash_lib.Std.Hash.state -> intro_pattern -> Ppx_hash_lib.Std.Hash.state
val hash_intro_pattern : intro_pattern -> Ppx_hash_lib.Std.Hash.hash_value
val compare_intro_pattern : intro_pattern -> intro_pattern -> int
val sexp_of_raw_red_expr : raw_red_expr -> Sexplib0.Sexp.t
val raw_red_expr_of_sexp : Sexplib0.Sexp.t -> raw_red_expr
val hash_fold_raw_red_expr : Ppx_hash_lib.Std.Hash.state -> raw_red_expr -> Ppx_hash_lib.Std.Hash.state
val hash_raw_red_expr : raw_red_expr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_raw_red_expr : raw_red_expr -> raw_red_expr -> int
val sexp_of_glob_red_expr : glob_red_expr -> Sexplib0.Sexp.t
val glob_red_expr_of_sexp : Sexplib0.Sexp.t -> glob_red_expr
val hash_fold_glob_red_expr : Ppx_hash_lib.Std.Hash.state -> glob_red_expr -> Ppx_hash_lib.Std.Hash.state
val hash_glob_red_expr : glob_red_expr -> Ppx_hash_lib.Std.Hash.hash_value
val compare_glob_red_expr : glob_red_expr -> glob_red_expr -> 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