coq-serapi 8.17.0+0.17.1 · OCaml Package

module CAst = Ser_cAst

module Names = Ser_names

module Namegen = Ser_namegen

module EConstr = Ser_eConstr

type 'a intro_pattern_action_expr = 'a Tactypes.intro_pattern_action_expr =

| IntroWildcard
| IntroOrAndPattern of 'a or_and_intro_pattern_expr
| IntroInjection of 'a intro_pattern_expr CAst.t list
| IntroApplyOn of 'a CAst.t * 'a intro_pattern_expr CAst.t
| IntroRewrite of bool

and 'a intro_pattern_expr = 'a Tactypes.intro_pattern_expr =

| IntroForthcoming of bool
| IntroNaming of Namegen.intro_pattern_naming_expr
| IntroAction of 'a intro_pattern_action_expr

and 'a or_and_intro_pattern_expr = 'a Tactypes.or_and_intro_pattern_expr =

| IntroOrPattern of 'a intro_pattern_expr CAst.t list list
| IntroAndPattern of 'a intro_pattern_expr CAst.t list

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

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

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

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

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

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

val intro_pattern_action_expr_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a intro_pattern_action_expr ->
  Yojson.Safe.t

val intro_pattern_action_expr_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a intro_pattern_action_expr Ppx_deriving_yojson_runtime.error_or

val intro_pattern_expr_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a intro_pattern_expr ->
  Yojson.Safe.t

val intro_pattern_expr_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a intro_pattern_expr Ppx_deriving_yojson_runtime.error_or

val or_and_intro_pattern_expr_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a or_and_intro_pattern_expr ->
  Yojson.Safe.t

val or_and_intro_pattern_expr_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a or_and_intro_pattern_expr Ppx_deriving_yojson_runtime.error_or

val hash_fold_intro_pattern_action_expr : 
  'a. (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a intro_pattern_action_expr ->
  Base.Hash.state

val hash_fold_intro_pattern_expr : 
  'a. (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a intro_pattern_expr ->
  Base.Hash.state

val hash_fold_or_and_intro_pattern_expr : 
  'a. (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a or_and_intro_pattern_expr ->
  Base.Hash.state

val compare_intro_pattern_action_expr : 
  'a. ('a -> 'a -> int) ->
  'a intro_pattern_action_expr ->
  'a intro_pattern_action_expr ->
  int

val compare_intro_pattern_expr : 
  'a. ('a -> 'a -> int) ->
  'a intro_pattern_expr ->
  'a intro_pattern_expr ->
  int

val compare_or_and_intro_pattern_expr : 
  'a. ('a -> 'a -> int) ->
  'a or_and_intro_pattern_expr ->
  'a or_and_intro_pattern_expr ->
  int

type quantified_hypothesis = Tactypes.quantified_hypothesis =

| AnonHyp of int
| NamedHyp of Names.lident

val quantified_hypothesis_of_sexp : Sexplib0.Sexp.t -> quantified_hypothesis

val sexp_of_quantified_hypothesis : quantified_hypothesis -> Sexplib0.Sexp.t

val quantified_hypothesis_to_yojson : quantified_hypothesis -> Yojson.Safe.t

val quantified_hypothesis_of_yojson : 
  Yojson.Safe.t ->
  quantified_hypothesis Ppx_deriving_yojson_runtime.error_or

val hash_fold_quantified_hypothesis : 
  Base.Hash.state ->
  quantified_hypothesis ->
  Base.Hash.state

val hash_quantified_hypothesis : quantified_hypothesis -> Base.Hash.hash_value

val compare_quantified_hypothesis : 
  quantified_hypothesis ->
  quantified_hypothesis ->
  int

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

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

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

val explicit_bindings_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a explicit_bindings ->
  Yojson.Safe.t

val explicit_bindings_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a explicit_bindings Ppx_deriving_yojson_runtime.error_or

val hash_fold_explicit_bindings : 
  'a. (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a explicit_bindings ->
  Base.Hash.state

val compare_explicit_bindings : 
  'a. ('a -> 'a -> int) ->
  'a explicit_bindings ->
  'a explicit_bindings ->
  int

type 'a bindings = 'a Tactypes.bindings =

| ImplicitBindings of 'a list
| ExplicitBindings of 'a explicit_bindings
| NoBindings

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

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

val bindings_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a bindings ->
  Yojson.Safe.t

val bindings_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a bindings Ppx_deriving_yojson_runtime.error_or

val hash_fold_bindings : 
  'a. (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a bindings ->
  Base.Hash.state

val compare_bindings : 
  'a. ('a -> 'a -> int) ->
  'a bindings ->
  'a bindings ->
  int

type 'a with_bindings = 'a * 'a bindings

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

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

val with_bindings_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a with_bindings ->
  Yojson.Safe.t

val with_bindings_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a with_bindings Ppx_deriving_yojson_runtime.error_or

val hash_fold_with_bindings : 
  'a. (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a with_bindings ->
  Base.Hash.state

val compare_with_bindings : 
  'a. ('a -> 'a -> int) ->
  'a with_bindings ->
  'a with_bindings ->
  int

module DO : sig ... end

module B : sig ... end

type 'a delayed_open = 'a B.t

val delayed_open_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a delayed_open

val sexp_of_delayed_open : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a delayed_open ->
  Sexplib0.Sexp.t

val delayed_open_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a delayed_open ->
  Yojson.Safe.t

val delayed_open_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a delayed_open Ppx_deriving_yojson_runtime.error_or

val hash_fold_delayed_open : 
  'a. (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a delayed_open ->
  Base.Hash.state

val compare_delayed_open : 
  'a. ('a -> 'a -> int) ->
  'a delayed_open ->
  'a delayed_open ->
  int

type delayed_open_constr = EConstr.constr delayed_open

val delayed_open_constr_of_sexp : Sexplib0.Sexp.t -> delayed_open_constr

val sexp_of_delayed_open_constr : delayed_open_constr -> Sexplib0.Sexp.t

val delayed_open_constr_to_yojson : delayed_open_constr -> Yojson.Safe.t

val delayed_open_constr_of_yojson : 
  Yojson.Safe.t ->
  delayed_open_constr Ppx_deriving_yojson_runtime.error_or

val hash_fold_delayed_open_constr : 
  Base.Hash.state ->
  delayed_open_constr ->
  Base.Hash.state

val hash_delayed_open_constr : delayed_open_constr -> Base.Hash.hash_value

val compare_delayed_open_constr : 
  delayed_open_constr ->
  delayed_open_constr ->
  int

type delayed_open_constr_with_bindings =
  EConstr.constr with_bindings delayed_open

val delayed_open_constr_with_bindings_of_sexp : 
  Sexplib0.Sexp.t ->
  delayed_open_constr_with_bindings

val sexp_of_delayed_open_constr_with_bindings : 
  delayed_open_constr_with_bindings ->
  Sexplib0.Sexp.t

val delayed_open_constr_with_bindings_to_yojson : 
  delayed_open_constr_with_bindings ->
  Yojson.Safe.t

val delayed_open_constr_with_bindings_of_yojson : 
  Yojson.Safe.t ->
  delayed_open_constr_with_bindings Ppx_deriving_yojson_runtime.error_or

val _ : 
  Yojson.Safe.t ->
  delayed_open_constr_with_bindings Ppx_deriving_yojson_runtime.error_or

val hash_fold_delayed_open_constr_with_bindings : 
  Base.Hash.state ->
  delayed_open_constr_with_bindings ->
  Base.Hash.state

val hash_delayed_open_constr_with_bindings : 
  delayed_open_constr_with_bindings ->
  Base.Hash.hash_value

val compare_delayed_open_constr_with_bindings : 
  delayed_open_constr_with_bindings ->
  delayed_open_constr_with_bindings ->
  int

package coq-serapi