coq-serapi 8.15.0+0.15.0 · OCaml Package

module Loc = Serlib.Ser_loc

module Names = Serlib.Ser_names

module Locus = Serlib.Ser_locus

module Constrexpr = Serlib.Ser_constrexpr

module Genintern = Serlib.Ser_genintern

module Geninterp = Serlib.Ser_geninterp

module Ssrmatching_plugin : sig ... end

module Ltac_plugin : sig ... end

type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind

val ssrtermkind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrtermkind

val sexp_of_ssrtermkind : ssrtermkind -> Ppx_sexp_conv_lib.Sexp.t

module Proofview : sig ... end

type ssrhyp =

| SsrHyp of Names.Id.t Loc.located

val ssrhyp_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyp

val sexp_of_ssrhyp : ssrhyp -> Ppx_sexp_conv_lib.Sexp.t

type ssrhyp_or_id =

| Hyp of ssrhyp
| Id of ssrhyp

val ssrhyp_or_id_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyp_or_id

val sexp_of_ssrhyp_or_id : ssrhyp_or_id -> Ppx_sexp_conv_lib.Sexp.t

type ssrhyps = ssrhyp list

val ssrhyps_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyps

val sexp_of_ssrhyps : ssrhyps -> Ppx_sexp_conv_lib.Sexp.t

type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir =

| L2R
| R2L

val ssrdir_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrdir

val sexp_of_ssrdir : ssrdir -> Ppx_sexp_conv_lib.Sexp.t

type ssrsimpl =

| Simpl of int
| Cut of int
| SimplCut of int * int
| Nop

val ssrsimpl_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrsimpl

val sexp_of_ssrsimpl : ssrsimpl -> Ppx_sexp_conv_lib.Sexp.t

type ssrmmod =

| May
| Must
| Once

val ssrmmod_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrmmod

val sexp_of_ssrmmod : ssrmmod -> Ppx_sexp_conv_lib.Sexp.t

type ssrmult = int * ssrmmod

val ssrmult_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrmult

val sexp_of_ssrmult : ssrmult -> Ppx_sexp_conv_lib.Sexp.t

type ssrocc = (bool * int list) option

val ssrocc_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrocc

val sexp_of_ssrocc : ssrocc -> Ppx_sexp_conv_lib.Sexp.t

type ssrindex = int Locus.or_var

val ssrindex_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrindex

val sexp_of_ssrindex : ssrindex -> Ppx_sexp_conv_lib.Sexp.t

type ssrclear = ssrhyps

val ssrclear_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrclear

val sexp_of_ssrclear : ssrclear -> Ppx_sexp_conv_lib.Sexp.t

type ssrdocc = ssrclear option * ssrocc

val ssrdocc_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrdocc

val sexp_of_ssrdocc : ssrdocc -> Ppx_sexp_conv_lib.Sexp.t

type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr

val ssrterm_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrterm

val sexp_of_ssrterm : ssrterm -> Ppx_sexp_conv_lib.Sexp.t

type ast_glob_env = {

ast_ltacvars : Names.Id.Set.t;
ast_extra : Genintern.Store.t;
ast_intern_sign : Genintern.intern_variable_status;

}

val ast_glob_env_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ast_glob_env

val sexp_of_ast_glob_env : ast_glob_env -> Ppx_sexp_conv_lib.Sexp.t

type ast_closure_term = {

body : Constrexpr.constr_expr;
glob_env : ast_glob_env option;
interp_env : Geninterp.interp_sign option;
annotation : [ `At | `DoubleParens | `Parens | `None ];

}

val ast_closure_term_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ast_closure_term

val sexp_of_ast_closure_term : ast_closure_term -> Ppx_sexp_conv_lib.Sexp.t

type ssrview = ast_closure_term list

val ssrview_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrview

val sexp_of_ssrview : ssrview -> Ppx_sexp_conv_lib.Sexp.t

type anon_kind =

| One of string option
| Drop
| All
| Temporary

val anon_kind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> anon_kind

val sexp_of_anon_kind : anon_kind -> Ppx_sexp_conv_lib.Sexp.t

type id_block =

| Prefix of Names.Id.t
| SuffixId of Names.Id.t
| SuffixNum of int

val id_block_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> id_block

val sexp_of_id_block : id_block -> Ppx_sexp_conv_lib.Sexp.t

type ssripat =

| IPatNoop
| IPatId of Names.Id.t
| IPatAnon of anon_kind
| IPatDispatch of ssripatss_or_block
| IPatCase of ssripatss_or_block
| IPatInj of ssripatss
| IPatRewrite of ssrocc * ssrdir
| IPatView of ssrview
| IPatClear of ssrclear
| IPatSimpl of ssrsimpl
| IPatAbstractVars of Names.Id.t list
| IPatFastNondep

and ssripats = ssripat list

and ssripatss = ssripats list

and ssripatss_or_block =

| Block of id_block
| Regular of ssripats list

val ssripat_of_sexp : Sexplib0.Sexp.t -> ssripat

val ssripats_of_sexp : Sexplib0.Sexp.t -> ssripats

val ssripatss_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssripatss

val ssripatss_or_block_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssripatss_or_block

val sexp_of_ssripat : ssripat -> Sexplib0.Sexp.t

val sexp_of_ssripats : ssripats -> Sexplib0.Sexp.t

val sexp_of_ssripatss : ssripatss -> Ppx_sexp_conv_lib.Sexp.t

val sexp_of_ssripatss_or_block : ssripatss_or_block -> Ppx_sexp_conv_lib.Sexp.t

type ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats

val ssrhpats_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhpats

val sexp_of_ssrhpats : ssrhpats -> Ppx_sexp_conv_lib.Sexp.t

type ssrhpats_wtransp = bool * ssrhpats

val ssrhpats_wtransp_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhpats_wtransp

val sexp_of_ssrhpats_wtransp : ssrhpats_wtransp -> Ppx_sexp_conv_lib.Sexp.t

type ssrintrosarg = Ltac_plugin.Tacexpr.raw_tactic_expr * ssripats

val ssrintrosarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrintrosarg

val sexp_of_ssrintrosarg : ssrintrosarg -> Ppx_sexp_conv_lib.Sexp.t

type ssrfwdid = Names.Id.t

val ssrfwdid_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdid

val sexp_of_ssrfwdid : ssrfwdid -> Ppx_sexp_conv_lib.Sexp.t

type 'term ssrbind =

| Bvar of Names.Name.t
| Bdecl of Names.Name.t list * 'term
| Bdef of Names.Name.t * 'term option * 'term
| Bstruct of Names.Name.t
| Bcast of 'term

val ssrbind_of_sexp : 
  'term. (Ppx_sexp_conv_lib.Sexp.t -> 'term) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'term ssrbind

val sexp_of_ssrbind : 
  'term. ('term -> Ppx_sexp_conv_lib.Sexp.t) ->
  'term ssrbind ->
  Ppx_sexp_conv_lib.Sexp.t

type ssrbindfmt =

| BFvar
| BFdecl of int
| BFcast
| BFdef
| BFrec of bool * bool

val ssrbindfmt_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrbindfmt

val sexp_of_ssrbindfmt : ssrbindfmt -> Ppx_sexp_conv_lib.Sexp.t

type 'term ssrbindval = 'term ssrbind list * 'term

val ssrbindval_of_sexp : 
  'term. (Ppx_sexp_conv_lib.Sexp.t -> 'term) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'term ssrbindval

val sexp_of_ssrbindval : 
  'term. ('term -> Ppx_sexp_conv_lib.Sexp.t) ->
  'term ssrbindval ->
  Ppx_sexp_conv_lib.Sexp.t

type ssrfwdkind =

| FwdHint of string * bool
| FwdHave
| FwdPose

val ssrfwdkind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdkind

val sexp_of_ssrfwdkind : ssrfwdkind -> Ppx_sexp_conv_lib.Sexp.t

type ssrfwdfmt = ssrfwdkind * ssrbindfmt list

val ssrfwdfmt_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdfmt

val sexp_of_ssrfwdfmt : ssrfwdfmt -> Ppx_sexp_conv_lib.Sexp.t

type ssrclseq =

| InGoal
| InHyps
| InHypsGoal
| InHypsSeqGoal
| InSeqGoal
| InHypsSeq
| InAll
| InAllHyps

val ssrclseq_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrclseq

val sexp_of_ssrclseq : ssrclseq -> Ppx_sexp_conv_lib.Sexp.t

type 'tac ssrhint = bool * 'tac option list

val ssrhint_of_sexp : 
  'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'tac ssrhint

val sexp_of_ssrhint : 
  'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) ->
  'tac ssrhint ->
  Ppx_sexp_conv_lib.Sexp.t

type 'tac fwdbinders =
  bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))

val fwdbinders_of_sexp : 
  'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'tac fwdbinders

val sexp_of_fwdbinders : 
  'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) ->
  'tac fwdbinders ->
  Ppx_sexp_conv_lib.Sexp.t

type 'tac ffwbinders =
  ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)

val ffwbinders_of_sexp : 
  'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'tac ffwbinders

val sexp_of_ffwbinders : 
  'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) ->
  'tac ffwbinders ->
  Ppx_sexp_conv_lib.Sexp.t

type clause =
  ssrclear
  * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option)
      option

val clause_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> clause

val sexp_of_clause : clause -> Ppx_sexp_conv_lib.Sexp.t

type clauses = clause list * ssrclseq

val clauses_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> clauses

val sexp_of_clauses : clauses -> Ppx_sexp_conv_lib.Sexp.t

type wgen =
  ssrclear
  * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option)
      option

val wgen_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> wgen

val sexp_of_wgen : wgen -> Ppx_sexp_conv_lib.Sexp.t

type 'a ssrdoarg = ((ssrindex * ssrmmod) * 'a ssrhint) * clauses

val ssrdoarg_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a ssrdoarg

val sexp_of_ssrdoarg : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a ssrdoarg ->
  Ppx_sexp_conv_lib.Sexp.t

type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)

val ssrseqarg_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a ssrseqarg

val sexp_of_ssrseqarg : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a ssrseqarg ->
  Ppx_sexp_conv_lib.Sexp.t

type 'a ssragens = (ssrdocc * 'a) list list * ssrclear

val ssragens_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a ssragens

val sexp_of_ssragens : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a ssragens ->
  Ppx_sexp_conv_lib.Sexp.t

type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats)

val ssrapplyarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrapplyarg

val sexp_of_ssrapplyarg : ssrapplyarg -> Ppx_sexp_conv_lib.Sexp.t

type 'a ssrcasearg = ssripat option * ('a * ssripats)

val ssrcasearg_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a ssrcasearg

val sexp_of_ssrcasearg : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a ssrcasearg ->
  Ppx_sexp_conv_lib.Sexp.t

type 'a ssrmovearg = ssrview * 'a ssrcasearg

val ssrmovearg_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a ssrmovearg

val sexp_of_ssrmovearg : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a ssrmovearg ->
  Ppx_sexp_conv_lib.Sexp.t