coq-serapi 8.9.0+0.6.0 · OCaml Package

module CAst = Ser_cAst

module Names = Ser_names

module Namegen = Ser_namegen

type 'a intro_pattern_action_expr = 'a Tactypes.intro_pattern_action_expr =

and 'a intro_pattern_expr = 'a Tactypes.intro_pattern_expr =

and 'a or_and_intro_pattern_expr = 'a Tactypes.or_and_intro_pattern_expr =

val intro_pattern_action_expr_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a intro_pattern_action_expr

val intro_pattern_expr_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a intro_pattern_expr

val or_and_intro_pattern_expr_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a or_and_intro_pattern_expr

val sexp_of_intro_pattern_action_expr : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a intro_pattern_action_expr ->
  Ppx_sexp_conv_lib.Sexp.t

val sexp_of_intro_pattern_expr : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a intro_pattern_expr ->
  Ppx_sexp_conv_lib.Sexp.t

val sexp_of_or_and_intro_pattern_expr : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a or_and_intro_pattern_expr ->
  Ppx_sexp_conv_lib.Sexp.t

type quantified_hypothesis = Tactypes.quantified_hypothesis =

val quantified_hypothesis_of_sexp : 
  Ppx_sexp_conv_lib.Sexp.t ->
  quantified_hypothesis

val sexp_of_quantified_hypothesis : 
  quantified_hypothesis ->
  Ppx_sexp_conv_lib.Sexp.t

type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list

val explicit_bindings_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a explicit_bindings

val sexp_of_explicit_bindings : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a explicit_bindings ->
  Ppx_sexp_conv_lib.Sexp.t

type 'a bindings = 'a Tactypes.bindings =

val bindings_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a bindings

val sexp_of_bindings : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a bindings ->
  Ppx_sexp_conv_lib.Sexp.t

type 'a with_bindings = 'a * 'a bindings

val with_bindings_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a with_bindings

val sexp_of_with_bindings : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a with_bindings ->
  Ppx_sexp_conv_lib.Sexp.t

type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a

val sexp_of_delayed_open : 'a -> 'b -> Sexplib.Sexp.t

val delayed_open_of_sexp : 'a -> Sexplib.Sexp.t -> 'b

package coq-serapi