package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Names = Ser_names
type vernac_keep_as = Vernacextend.vernac_keep_as =
  1. | VtKeepAxiom
  2. | VtKeepDefined
  3. | VtKeepOpaque
and vernac_qed_type = Vernacextend.vernac_qed_type =
  1. | VtKeep of vernac_keep_as
  2. | VtDrop
and vernac_when = Vernacextend.vernac_when =
  1. | VtNow
  2. | VtLater
and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list * vernac_when
and opacity_guarantee = Vernacextend.opacity_guarantee =
  1. | GuaranteesOpacity
  2. | Doesn'tGuaranteeOpacity
and solving_tac = bool
and anon_abstracting_tac = bool
and proof_block_name = string
val vernac_keep_as_of_sexp : Sexplib0.Sexp.t -> vernac_keep_as
val vernac_qed_type_of_sexp : Sexplib0.Sexp.t -> vernac_qed_type
val vernac_when_of_sexp : Sexplib0.Sexp.t -> vernac_when
val vernac_start_of_sexp : Sexplib0.Sexp.t -> vernac_start
val vernac_sideff_type_of_sexp : Sexplib0.Sexp.t -> vernac_sideff_type
val opacity_guarantee_of_sexp : Sexplib0.Sexp.t -> opacity_guarantee
val solving_tac_of_sexp : Sexplib0.Sexp.t -> solving_tac
val anon_abstracting_tac_of_sexp : Sexplib0.Sexp.t -> anon_abstracting_tac
val proof_block_name_of_sexp : Sexplib0.Sexp.t -> proof_block_name
val sexp_of_vernac_keep_as : vernac_keep_as -> Sexplib0.Sexp.t
val sexp_of_vernac_qed_type : vernac_qed_type -> Sexplib0.Sexp.t
val sexp_of_vernac_when : vernac_when -> Sexplib0.Sexp.t
val sexp_of_vernac_start : vernac_start -> Sexplib0.Sexp.t
val sexp_of_vernac_sideff_type : vernac_sideff_type -> Sexplib0.Sexp.t
val sexp_of_opacity_guarantee : opacity_guarantee -> Sexplib0.Sexp.t
val sexp_of_solving_tac : solving_tac -> Sexplib0.Sexp.t
val sexp_of_anon_abstracting_tac : anon_abstracting_tac -> Sexplib0.Sexp.t
val sexp_of_proof_block_name : proof_block_name -> Sexplib0.Sexp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct