package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Serlib.Ser_vernacextendSource

Sourcemodule Names = Ser_names
Sourcetype vernac_keep_as = Vernacextend.vernac_keep_as =
  1. | VtKeepAxiom
  2. | VtKeepDefined
  3. | VtKeepOpaque
Sourceand vernac_qed_type = Vernacextend.vernac_qed_type =
  1. | VtKeep of vernac_keep_as
  2. | VtDrop
Sourceand vernac_when = Vernacextend.vernac_when =
  1. | VtNow
  2. | VtLater
Sourceand vernac_start = opacity_guarantee * Names.Id.t list
Sourceand vernac_sideff_type = Names.Id.t list * vernac_when
Sourceand opacity_guarantee = Vernacextend.opacity_guarantee =
  1. | GuaranteesOpacity
  2. | Doesn'tGuaranteeOpacity
Sourceand solving_tac = bool
Sourceand anon_abstracting_tac = bool
Sourceand proof_block_name = string
Sourceval vernac_keep_as_of_sexp : Sexplib0.Sexp.t -> vernac_keep_as
Sourceval vernac_qed_type_of_sexp : Sexplib0.Sexp.t -> vernac_qed_type
Sourceval vernac_when_of_sexp : Sexplib0.Sexp.t -> vernac_when
Sourceval vernac_start_of_sexp : Sexplib0.Sexp.t -> vernac_start
Sourceval vernac_sideff_type_of_sexp : Sexplib0.Sexp.t -> vernac_sideff_type
Sourceval opacity_guarantee_of_sexp : Sexplib0.Sexp.t -> opacity_guarantee
Sourceval solving_tac_of_sexp : Sexplib0.Sexp.t -> solving_tac
Sourceval anon_abstracting_tac_of_sexp : Sexplib0.Sexp.t -> anon_abstracting_tac
Sourceval proof_block_name_of_sexp : Sexplib0.Sexp.t -> proof_block_name
Sourceval sexp_of_vernac_keep_as : vernac_keep_as -> Sexplib0.Sexp.t
Sourceval sexp_of_vernac_qed_type : vernac_qed_type -> Sexplib0.Sexp.t
Sourceval sexp_of_vernac_when : vernac_when -> Sexplib0.Sexp.t
Sourceval sexp_of_vernac_start : vernac_start -> Sexplib0.Sexp.t
Sourceval sexp_of_vernac_sideff_type : vernac_sideff_type -> Sexplib0.Sexp.t
Sourceval sexp_of_opacity_guarantee : opacity_guarantee -> Sexplib0.Sexp.t
Sourceval sexp_of_solving_tac : solving_tac -> Sexplib0.Sexp.t
Sourceval sexp_of_anon_abstracting_tac : anon_abstracting_tac -> Sexplib0.Sexp.t
Sourceval 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