package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = Ltac2_plugin.Tac2expr.raw_tacexpr_r
type _t =
  1. | CTacAtm of Ltac2_plugin.Tac2expr.atom
  2. | CTacRef of Ltac2_plugin.Tac2expr.tacref Ltac2_plugin.Tac2expr.or_relid
  3. | CTacCst of Ltac2_plugin.Tac2expr.ltac_constructor Ltac2_plugin.Tac2expr.or_tuple Ltac2_plugin.Tac2expr.or_relid
  4. | CTacFun of Ltac2_plugin.Tac2expr.raw_patexpr list * raw_tacexpr
  5. | CTacApp of raw_tacexpr * raw_tacexpr list
  6. | CTacSyn of (Names.lname * raw_tacexpr) list * Names.KerName.t
  7. | CTacLet of Ltac2_plugin.Tac2expr.rec_flag * (Ltac2_plugin.Tac2expr.raw_patexpr * raw_tacexpr) list * raw_tacexpr
  8. | CTacCnv of raw_tacexpr * Ltac2_plugin.Tac2expr.raw_typexpr
  9. | CTacSeq of raw_tacexpr * raw_tacexpr
  10. | CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
  11. | CTacCse of raw_tacexpr * raw_taccase list
  12. | CTacRec of raw_tacexpr option * raw_recexpr
  13. | CTacPrj of raw_tacexpr * Ltac2_plugin.Tac2expr.ltac_projection Ltac2_plugin.Tac2expr.or_relid
  14. | CTacSet of raw_tacexpr * Ltac2_plugin.Tac2expr.ltac_projection Ltac2_plugin.Tac2expr.or_relid * raw_tacexpr
  15. | CTacExt of int * Obj.t
  16. | CTacGlb of int * (Names.lname * raw_tacexpr * int Ltac2_plugin.Tac2expr.glb_typexpr option) list * Ltac2_plugin.Tac2expr.glb_tacexpr * int Ltac2_plugin.Tac2expr.glb_typexpr
and raw_tacexpr = _t CAst.t
and raw_taccase = Ltac2_plugin.Tac2expr.raw_patexpr * raw_tacexpr
and raw_recexpr = (Ltac2_plugin.Tac2expr.ltac_projection Ltac2_plugin.Tac2expr.or_relid * raw_tacexpr) list
val _t_of_sexp : Sexplib0__.Sexp.t -> _t
val raw_tacexpr_of_sexp : Sexplib0__.Sexp.t -> raw_tacexpr
val raw_taccase_of_sexp : Sexplib0__.Sexp.t -> raw_taccase
val raw_recexpr_of_sexp : Sexplib0.Sexp.t -> raw_recexpr
val sexp_of__t : _t -> Sexplib0__.Sexp.t
val sexp_of_raw_tacexpr : raw_tacexpr -> Sexplib0__.Sexp.t
val sexp_of_raw_taccase : raw_taccase -> Sexplib0__.Sexp.t
val sexp_of_raw_recexpr : raw_recexpr -> Sexplib0.Sexp.t
val _t_to_yojson : _t -> Yojson.Safe.t
val _t_of_yojson : Yojson.Safe.t -> _t Ppx_deriving_yojson_runtime.error_or
val raw_tacexpr_to_yojson : raw_tacexpr -> Yojson.Safe.t
val raw_tacexpr_of_yojson : Yojson.Safe.t -> raw_tacexpr Ppx_deriving_yojson_runtime.error_or
val raw_taccase_to_yojson : raw_taccase -> Yojson.Safe.t
val raw_taccase_of_yojson : Yojson.Safe.t -> raw_taccase Ppx_deriving_yojson_runtime.error_or
val raw_recexpr_to_yojson : raw_recexpr -> Yojson.Safe.t
val raw_recexpr_of_yojson : Yojson.Safe.t -> raw_recexpr Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> raw_recexpr Ppx_deriving_yojson_runtime.error_or
val hash_fold__t : _t Base__Ppx_hash_lib.hash_fold
val hash_fold_raw_tacexpr : raw_tacexpr Base__Hash.folder
val hash_fold_raw_taccase : raw_taccase Base__Hash.folder
val hash_fold_raw_recexpr : Ppx_hash_lib.Std.Hash.state -> raw_recexpr -> Ppx_hash_lib.Std.Hash.state
val hash__t : _t -> Ppx_hash_lib.Std.Hash.hash_value
val hash_raw_tacexpr : raw_tacexpr -> Ppx_hash_lib.Std.Hash.hash_value
val hash_raw_taccase : raw_taccase -> Ppx_hash_lib.Std.Hash.hash_value
val hash_raw_recexpr : raw_recexpr -> Ppx_hash_lib.Std.Hash.hash_value
val compare__t : _t -> _t -> int
val compare_raw_tacexpr : raw_tacexpr -> raw_tacexpr -> int
val compare_raw_taccase : raw_taccase -> raw_taccase -> int
val compare_raw_recexpr : raw_recexpr -> raw_recexpr -> int
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