coq-lsp 0.2.2+8.20 (latest)

coq-lsp

module Ssreflect_plugin : sig ... end

module Wrap : sig ... end

include module type of struct include Wrap end

include module type of Ssreflect_plugin.Ssrast

type ssrhyp = Ssreflect_plugin.Ssrast.ssrhyp =

| SsrHyp of Names.Id.t Loc.located

type ssrhyp_or_id = Ssreflect_plugin.Ssrast.ssrhyp_or_id =

| Hyp of ssrhyp
| Id of ssrhyp

type ssrhyps = ssrhyp list

type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir =

| L2R
| R2L

type ssrsimpl = Ssreflect_plugin.Ssrast.ssrsimpl =

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

type ssrmmod = Ssreflect_plugin.Ssrast.ssrmmod =

| May
| Must
| Once

type ssrmult = int * ssrmmod

type ssrocc = (bool * int list) option

Occurrence switch

, all is Some(false,)

type ssrindex = int Locus.or_var

type ssrclear = ssrhyps

type ssrdocc = ssrclear option * ssrocc

type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind

type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr

type ast_glob_env = Ssreflect_plugin.Ssrast.ast_glob_env = {

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

}

type ast_closure_term = Ssreflect_plugin.Ssrast.ast_closure_term = {

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

}

type ssrview = ast_closure_term list

type id_block = Ssreflect_plugin.Ssrast.id_block =

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

type anon_kind = Ssreflect_plugin.Ssrast.anon_kind =

| One of string option
| Drop
| All
| Temporary

type ssripat = Ssreflect_plugin.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

and ssripats = ssripat list

and ssripatss = ssripats list

and ssripatss_or_block = Ssreflect_plugin.Ssrast.ssripatss_or_block =

| Block of id_block
| Regular of ssripats list

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

type ssrhpats_wtransp = bool * ssrhpats

type ssrintrosarg = Ltac_plugin.Tacexpr.raw_tactic_expr * ssripats

type ssrfwdid = Names.Id.t

type 'term ssrbind = 'term Ssreflect_plugin.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

Binders (for fwd tactics)

type ssrbindfmt = Ssreflect_plugin.Ssrast.ssrbindfmt =

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

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

type ssrfwdkind = Ssreflect_plugin.Ssrast.ssrfwdkind =

| FwdHint of string * bool
| FwdHave
| FwdPose

Forward chaining argument

type ssrfwdfmt = ssrfwdkind * ssrbindfmt list

type ssrclseq = Ssreflect_plugin.Ssrast.ssrclseq =

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

type 'tac ssrhint = bool * 'tac option list

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

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

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

type clauses = clause list * ssrclseq

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

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

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

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

type 'a ssrmovearg = ssrview * 'a ssrcasearg

type ssrdgens = Ssreflect_plugin.Ssrast.ssrdgens = {

dgens : (ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list;
gens : (ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list;
clr : ssrclear;

}

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

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

type gist = Ltac_plugin.Tacintern.glob_sign

type ist = Ltac_plugin.Tacinterp.interp_sign

type goal = Evar.t

package coq-lsp