Module `Serlib_ssr.Ser_ssrast`Source

Sourcemodule Loc = Serlib.Ser_loc

Sourcemodule Names = Serlib.Ser_names

Sourcemodule Locus = Serlib.Ser_locus

Sourcemodule Constrexpr = Serlib.Ser_constrexpr

Sourcemodule Genintern = Serlib.Ser_genintern

Sourcemodule Geninterp = Serlib.Ser_geninterp

Sourcemodule Ssrmatching_plugin : sig ... end

Sourcemodule Ltac_plugin : sig ... end

Sourcemodule Proofview : sig ... end

Sourcetype ssrhyp = Ssrast.ssrhyp =

| SsrHyp of Names.Id.t Loc.located

Sourceval ssrhyp_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyp

Sourceval sexp_of_ssrhyp : ssrhyp -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrhyp_or_id = Ssrast.ssrhyp_or_id =

| Hyp of ssrhyp
| Id of ssrhyp

Sourceval ssrhyp_or_id_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyp_or_id

Sourceval sexp_of_ssrhyp_or_id : ssrhyp_or_id -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrhyps = ssrhyp list

Sourceval ssrhyps_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyps

Sourceval sexp_of_ssrhyps : ssrhyps -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir =

| L2R
| R2L

Sourceval ssrdir_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrdir

Sourceval sexp_of_ssrdir : ssrdir -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrsimpl = Ssrast.ssrsimpl =

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

Sourceval ssrsimpl_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrsimpl

Sourceval sexp_of_ssrsimpl : ssrsimpl -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrmmod = Ssrast.ssrmmod =

| May
| Must
| Once

Sourceval ssrmmod_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrmmod

Sourceval sexp_of_ssrmmod : ssrmmod -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrmult = int * ssrmmod

Sourceval ssrmult_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrmult

Sourceval sexp_of_ssrmult : ssrmult -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrocc = (bool * int list) option

Sourceval ssrocc_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrocc

Sourceval sexp_of_ssrocc : ssrocc -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrindex = int Locus.or_var

Sourceval ssrindex_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrindex

Sourceval sexp_of_ssrindex : ssrindex -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrclear = ssrhyps

Sourceval ssrclear_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrclear

Sourceval sexp_of_ssrclear : ssrclear -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrdocc = ssrclear option * ssrocc

Sourceval ssrdocc_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrdocc

Sourceval sexp_of_ssrdocc : ssrdocc -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrtermkind = char

Sourceval ssrtermkind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrtermkind

Sourceval sexp_of_ssrtermkind : ssrtermkind -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrterm = ssrtermkind * Genintern.glob_constr_and_expr

Sourceval ssrterm_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrterm

Sourceval sexp_of_ssrterm : ssrterm -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ast_glob_env = Ssrast.ast_glob_env = {

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

}

Sourceval ast_glob_env_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ast_glob_env

Sourceval sexp_of_ast_glob_env : ast_glob_env -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ast_closure_term = Ssrast.ast_closure_term = {

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

}

Sourceval ast_closure_term_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ast_closure_term

Sourceval sexp_of_ast_closure_term : ast_closure_term -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrview = ast_closure_term list

Sourceval ssrview_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrview

Sourceval sexp_of_ssrview : ssrview -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype anon_kind = Ssrast.anon_kind =

| One of string option
| Drop
| All
| Temporary

Sourceval anon_kind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> anon_kind

Sourceval sexp_of_anon_kind : anon_kind -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype id_block = Ssrast.id_block =

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

Sourceval id_block_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> id_block

Sourceval sexp_of_id_block : id_block -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssripat = Ssrast.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

Sourceand ssripats = ssripat list

Sourceand ssripatss = ssripats list

Sourceand ssripatss_or_block = Ssrast.ssripatss_or_block =

| Block of id_block
| Regular of ssripats list

Sourceval ssripat_of_sexp : Sexplib0__.Sexp.t -> ssripat

Sourceval ssripats_of_sexp : Sexplib0__.Sexp.t -> ssripats

Sourceval ssripatss_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssripatss

Sourceval ssripatss_or_block_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssripatss_or_block

Sourceval sexp_of_ssripat : ssripat -> Sexplib0__.Sexp.t

Sourceval sexp_of_ssripats : ssripats -> Sexplib0__.Sexp.t

Sourceval sexp_of_ssripatss : ssripatss -> Ppx_sexp_conv_lib.Sexp.t

Sourceval sexp_of_ssripatss_or_block : ssripatss_or_block -> Ppx_sexp_conv_lib.Sexp.t

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

Sourceval ssrhpats_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhpats

Sourceval sexp_of_ssrhpats : ssrhpats -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrhpats_wtransp = bool * ssrhpats

Sourceval ssrhpats_wtransp_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhpats_wtransp

Sourceval sexp_of_ssrhpats_wtransp : ssrhpats_wtransp -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrintrosarg = Ltac_plugin.Tacexpr.raw_tactic_expr * ssripats

Sourceval ssrintrosarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrintrosarg

Sourceval sexp_of_ssrintrosarg : ssrintrosarg -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrfwdid = Names.Id.t

Sourceval ssrfwdid_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdid

Sourceval sexp_of_ssrfwdid : ssrfwdid -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype 'term ssrbind = 'term Ssrast.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

Source

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

Source

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

Sourcetype ssrbindfmt = Ssrast.ssrbindfmt =

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

Sourceval ssrbindfmt_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrbindfmt

Sourceval sexp_of_ssrbindfmt : ssrbindfmt -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype 'term ssrbindval = 'term ssrbind list * 'term

Source

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

Source

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

Sourcetype ssrfwdkind = Ssrast.ssrfwdkind =

| FwdHint of string * bool
| FwdHave
| FwdPose

Sourceval ssrfwdkind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdkind

Sourceval sexp_of_ssrfwdkind : ssrfwdkind -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrfwdfmt = ssrfwdkind * ssrbindfmt list

Sourceval ssrfwdfmt_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdfmt

Sourceval sexp_of_ssrfwdfmt : ssrfwdfmt -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssrclseq = Ssrast.ssrclseq =

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

Sourceval ssrclseq_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrclseq

Sourceval sexp_of_ssrclseq : ssrclseq -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype 'tac ssrhint = bool * 'tac option list

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Sourceval clause_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> clause

Sourceval sexp_of_clause : clause -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype clauses = clause list * ssrclseq

Sourceval clauses_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> clauses

Sourceval sexp_of_clauses : clauses -> Ppx_sexp_conv_lib.Sexp.t

Source

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

Sourceval wgen_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> wgen

Sourceval sexp_of_wgen : wgen -> Ppx_sexp_conv_lib.Sexp.t

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

Source

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

Source

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

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

Source

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

Source

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

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

Source

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

Source

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

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

Sourceval ssrapplyarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrapplyarg

Sourceval sexp_of_ssrapplyarg : ssrapplyarg -> Ppx_sexp_conv_lib.Sexp.t

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

Source

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

Source

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

Sourcetype 'a ssrmovearg = ssrview * 'a ssrcasearg

Source

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

Source

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/serlib_ssr/Serlib_ssr/Ser_ssrast/index.html

Module `Serlib_ssr.Ser_ssrast`Source

package coq-serapi

Install

Dune Dependency

Authors

Maintainers

Sources

doc/serlib_ssr/Serlib_ssr/Ser_ssrast/index.html

Module Serlib_ssr.Ser_ssrastSource

Module `Serlib_ssr.Ser_ssrast`Source