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 location_of_sexp : (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'b) -> Sexplib.Sexp.t -> ('a, 'b) location
val sexp_of_location : ('a -> Sexplib.Sexp.t) -> ('b -> Sexplib.Sexp.t) -> ('a, 'b) location -> Sexplib.Sexp.t
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 glob_tactic_expr_of_sexp : Sexplib.Sexp.t -> glob_tactic_expr
val sexp_of_glob_tactic_expr : glob_tactic_expr -> Sexplib.Sexp.t
type glob_atomic_tactic_expr = Ltac_plugin.Tacexpr.glob_atomic_tactic_expr
val glob_atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> glob_atomic_tactic_expr
val sexp_of_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> Sexplib.Sexp.t
val raw_tactic_expr_of_sexp : Sexplib.Sexp.t -> raw_tactic_expr
val sexp_of_raw_tactic_expr : raw_tactic_expr -> Sexplib.Sexp.t
type raw_atomic_tactic_expr = Ltac_plugin.Tacexpr.raw_atomic_tactic_expr
val raw_atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> raw_atomic_tactic_expr
val sexp_of_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> Sexplib.Sexp.t
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 tacdef_body_of_sexp : Sexplib.Sexp.t -> tacdef_body
val sexp_of_tacdef_body : tacdef_body -> Sexplib.Sexp.t
val intro_pattern_of_sexp : Sexplib.Sexp.t -> intro_pattern
val sexp_of_intro_pattern : intro_pattern -> Sexplib.Sexp.t
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