Module Serlib_ltac.Ser_tacexprSource

Sourcetype direction_flag = bool
Sourceval direction_flag_of_sexp : Sexplib.Sexp.t -> direction_flag
Sourceval sexp_of_direction_flag : direction_flag -> Sexplib.Sexp.t
Sourcetype lazy_flag = Ltac_plugin.Tacexpr.lazy_flag =
  1. | General
  2. | Select
  3. | Once
Sourceval lazy_flag_of_sexp : Sexplib.Sexp.t -> lazy_flag
Sourceval sexp_of_lazy_flag : lazy_flag -> Sexplib.Sexp.t
Sourcetype global_flag = Ltac_plugin.Tacexpr.global_flag =
  1. | TacGlobal
  2. | TacLocal
Sourceval global_flag_of_sexp : Sexplib.Sexp.t -> global_flag
Sourceval sexp_of_global_flag : global_flag -> Sexplib.Sexp.t
Sourcetype evars_flag = bool
Sourceval evars_flag_of_sexp : Sexplib.Sexp.t -> evars_flag
Sourceval sexp_of_evars_flag : evars_flag -> Sexplib.Sexp.t
Sourcetype rec_flag = bool
Sourceval rec_flag_of_sexp : Sexplib.Sexp.t -> rec_flag
Sourceval sexp_of_rec_flag : rec_flag -> Sexplib.Sexp.t
Sourcetype advanced_flag = bool
Sourceval advanced_flag_of_sexp : Sexplib.Sexp.t -> advanced_flag
Sourceval sexp_of_advanced_flag : advanced_flag -> Sexplib.Sexp.t
Sourcetype letin_flag = bool
Sourceval letin_flag_of_sexp : Sexplib.Sexp.t -> letin_flag
Sourceval sexp_of_letin_flag : letin_flag -> Sexplib.Sexp.t
Sourcetype clear_flag = bool option
Sourceval clear_flag_of_sexp : Sexplib.Sexp.t -> clear_flag
Sourceval sexp_of_clear_flag : clear_flag -> Sexplib.Sexp.t
Sourcetype ('c, 'd, 'id) inversion_strength = ('c, 'd, 'id) Ltac_plugin.Tacexpr.inversion_strength
Sourceval inversion_strength_of_sexp : (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> ('c, 'd, 'id) inversion_strength
Sourceval sexp_of_inversion_strength : ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('id -> Sexplib.Sexp.t) -> ('c, 'd, 'id) inversion_strength -> Sexplib.Sexp.t
Sourcetype ('a, 'b) location = ('a, 'b) Ltac_plugin.Tacexpr.location =
  1. | HypLocation of 'a
  2. | ConclLocation of 'b
Sourceval location_of_sexp : (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'b) -> Sexplib.Sexp.t -> ('a, 'b) location
Sourceval sexp_of_location : ('a -> Sexplib.Sexp.t) -> ('b -> Sexplib.Sexp.t) -> ('a, 'b) location -> Sexplib.Sexp.t
Sourcetype 'id message_token = 'id Ltac_plugin.Tacexpr.message_token
Sourceval message_token_of_sexp : (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> 'id message_token
Sourceval sexp_of_message_token : ('id -> Sexplib.Sexp.t) -> 'id message_token -> Sexplib.Sexp.t
Sourcetype ('dconstr, 'id) induction_clause = ('dconstr, 'id) Ltac_plugin.Tacexpr.induction_clause
Sourceval induction_clause_of_sexp : (Sexplib.Sexp.t -> 'dconstr) -> (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> ('dconstr, 'id) induction_clause
Sourceval sexp_of_induction_clause : ('dconstr -> Sexplib.Sexp.t) -> ('id -> Sexplib.Sexp.t) -> ('dconstr, 'id) induction_clause -> Sexplib.Sexp.t
Sourcetype ('constr, 'dconstr, 'id) induction_clause_list = ('constr, 'dconstr, 'id) Ltac_plugin.Tacexpr.induction_clause_list
Sourceval 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
Sourceval 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
Sourcetype 'a with_bindings_arg = 'a Ltac_plugin.Tacexpr.with_bindings_arg
Sourceval with_bindings_arg_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a with_bindings_arg
Sourceval sexp_of_with_bindings_arg : ('a -> Sexplib.Sexp.t) -> 'a with_bindings_arg -> Sexplib.Sexp.t
Sourcetype 'a match_pattern = 'a Ltac_plugin.Tacexpr.match_pattern
Sourceval match_pattern_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a match_pattern
Sourceval sexp_of_match_pattern : ('a -> Sexplib.Sexp.t) -> 'a match_pattern -> Sexplib.Sexp.t
Sourcetype 'a match_context_hyps = 'a Ltac_plugin.Tacexpr.match_context_hyps
Sourceval match_context_hyps_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a match_context_hyps
Sourceval sexp_of_match_context_hyps : ('a -> Sexplib.Sexp.t) -> 'a match_context_hyps -> Sexplib.Sexp.t
Sourcetype ('a, 't) match_rule = ('a, 't) Ltac_plugin.Tacexpr.match_rule
Sourceval match_rule_of_sexp : (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 't) -> Sexplib.Sexp.t -> ('a, 't) match_rule
Sourceval sexp_of_match_rule : ('a -> Sexplib.Sexp.t) -> ('t -> Sexplib.Sexp.t) -> ('a, 't) match_rule -> Sexplib.Sexp.t
Sourcetype ml_tactic_name = Ltac_plugin.Tacexpr.ml_tactic_name
Sourceval ml_tactic_name_of_sexp : Sexplib.Sexp.t -> ml_tactic_name
Sourceval sexp_of_ml_tactic_name : ml_tactic_name -> Sexplib.Sexp.t
Sourcetype 'd gen_atomic_tactic_expr = 'd Ltac_plugin.Tacexpr.gen_atomic_tactic_expr
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourcetype glob_tactic_expr = Ltac_plugin.Tacexpr.glob_tactic_expr
Sourceval glob_tactic_expr_of_sexp : Sexplib.Sexp.t -> glob_tactic_expr
Sourceval sexp_of_glob_tactic_expr : glob_tactic_expr -> Sexplib.Sexp.t
Sourcetype glob_atomic_tactic_expr = Ltac_plugin.Tacexpr.glob_atomic_tactic_expr
Sourceval glob_atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> glob_atomic_tactic_expr
Sourceval sexp_of_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> Sexplib.Sexp.t
Sourcetype raw_tactic_expr = Ltac_plugin.Tacexpr.raw_tactic_expr
Sourceval raw_tactic_expr_of_sexp : Sexplib.Sexp.t -> raw_tactic_expr
Sourceval sexp_of_raw_tactic_expr : raw_tactic_expr -> Sexplib.Sexp.t
Sourcetype raw_atomic_tactic_expr = Ltac_plugin.Tacexpr.raw_atomic_tactic_expr
Sourceval raw_atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> raw_atomic_tactic_expr
Sourceval sexp_of_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> Sexplib.Sexp.t
Sourcetype atomic_tactic_expr = Ltac_plugin.Tacexpr.atomic_tactic_expr
Sourceval atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> atomic_tactic_expr
Sourceval sexp_of_atomic_tactic_expr : atomic_tactic_expr -> Sexplib.Sexp.t
Sourcetype tacdef_body = Ltac_plugin.Tacexpr.tacdef_body
Sourceval tacdef_body_of_sexp : Sexplib.Sexp.t -> tacdef_body
Sourceval sexp_of_tacdef_body : tacdef_body -> Sexplib.Sexp.t
Sourcetype intro_pattern = Ltac_plugin.Tacexpr.intro_pattern
Sourceval intro_pattern_of_sexp : Sexplib.Sexp.t -> intro_pattern
Sourceval sexp_of_intro_pattern : intro_pattern -> Sexplib.Sexp.t
Sourcetype raw_red_expr = Ltac_plugin.Tacexpr.raw_red_expr
Sourceval raw_red_expr_of_sexp : Sexplib.Sexp.t -> raw_red_expr
Sourceval sexp_of_raw_red_expr : raw_red_expr -> Sexplib.Sexp.t
Sourcetype glob_red_expr = Ltac_plugin.Tacexpr.glob_red_expr
Sourceval glob_red_expr_of_sexp : Sexplib.Sexp.t -> glob_red_expr
Sourceval sexp_of_glob_red_expr : glob_red_expr -> Sexplib.Sexp.t