coq-serapi 8.17.0+0.17.0 · OCaml Package

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 =

| General
| Select
| 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 =

| TacGlobal
| 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 '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

type ml_tactic_name = Ltac_plugin.Tacexpr.ml_tactic_name

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 : 
  Base.Hash.state ->
  glob_tactic_expr ->
  Base.Hash.state

val hash_glob_tactic_expr : glob_tactic_expr -> Base.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 : 
  Base.Hash.state ->
  glob_atomic_tactic_expr ->
  Base.Hash.state

val hash_glob_atomic_tactic_expr : 
  glob_atomic_tactic_expr ->
  Base.Hash.hash_value

val compare_glob_atomic_tactic_expr : 
  glob_atomic_tactic_expr ->
  glob_atomic_tactic_expr ->
  int

type raw_tactic_expr = Ltac_plugin.Tacexpr.raw_tactic_expr

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 : 
  Base.Hash.state ->
  raw_tactic_expr ->
  Base.Hash.state

val hash_raw_tactic_expr : raw_tactic_expr -> Base.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 : 
  Base.Hash.state ->
  raw_atomic_tactic_expr ->
  Base.Hash.state

val hash_raw_atomic_tactic_expr : 
  raw_atomic_tactic_expr ->
  Base.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 : Base.Hash.state -> tacdef_body -> Base.Hash.state

val hash_tacdef_body : tacdef_body -> Base.Hash.hash_value

val compare_tacdef_body : tacdef_body -> tacdef_body -> int

type intro_pattern = Ltac_plugin.Tacexpr.intro_pattern

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 : 
  Base.Hash.state ->
  intro_pattern ->
  Base.Hash.state

val hash_intro_pattern : intro_pattern -> Base.Hash.hash_value

val compare_intro_pattern : intro_pattern -> intro_pattern -> int

type raw_red_expr = Ltac_plugin.Tacexpr.raw_red_expr

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 : Base.Hash.state -> raw_red_expr -> Base.Hash.state

val hash_raw_red_expr : raw_red_expr -> Base.Hash.hash_value

val compare_raw_red_expr : raw_red_expr -> raw_red_expr -> int

type glob_red_expr = Ltac_plugin.Tacexpr.glob_red_expr

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 : 
  Base.Hash.state ->
  glob_red_expr ->
  Base.Hash.state

val hash_glob_red_expr : glob_red_expr -> Base.Hash.hash_value

val compare_glob_red_expr : glob_red_expr -> glob_red_expr -> int

package coq-serapi