package coq-serapi

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

Module Ser_tac2expr.T2ESpecSource

Sourcetype t = Ltac2_plugin.Tac2expr.raw_tacexpr_r
Sourcetype _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. | CTacLet of Ltac2_plugin.Tac2expr.rec_flag * (Ltac2_plugin.Tac2expr.raw_patexpr * raw_tacexpr) list * raw_tacexpr
  7. | CTacCnv of raw_tacexpr * Ltac2_plugin.Tac2expr.raw_typexpr
  8. | CTacSeq of raw_tacexpr * raw_tacexpr
  9. | CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
  10. | CTacCse of raw_tacexpr * raw_taccase list
  11. | CTacRec of raw_recexpr
  12. | CTacPrj of raw_tacexpr * Ltac2_plugin.Tac2expr.ltac_projection Ltac2_plugin.Tac2expr.or_relid
  13. | CTacSet of raw_tacexpr * Ltac2_plugin.Tac2expr.ltac_projection Ltac2_plugin.Tac2expr.or_relid * raw_tacexpr
  14. | CTacExt of int * Obj.t
Sourceand raw_tacexpr = _t CAst.t
Sourceand raw_taccase = Ltac2_plugin.Tac2expr.raw_patexpr * raw_tacexpr
Sourceand raw_recexpr = (Ltac2_plugin.Tac2expr.ltac_projection Ltac2_plugin.Tac2expr.or_relid * raw_tacexpr) list
Sourceval _t_of_sexp : Sexplib0__.Sexp.t -> _t
Sourceval raw_tacexpr_of_sexp : Sexplib0__.Sexp.t -> raw_tacexpr
Sourceval raw_taccase_of_sexp : Sexplib0__.Sexp.t -> raw_taccase
Sourceval raw_recexpr_of_sexp : Sexplib0.Sexp.t -> raw_recexpr
Sourceval sexp_of__t : _t -> Sexplib0__.Sexp.t
Sourceval sexp_of_raw_tacexpr : raw_tacexpr -> Sexplib0__.Sexp.t
Sourceval sexp_of_raw_taccase : raw_taccase -> Sexplib0__.Sexp.t
Sourceval sexp_of_raw_recexpr : raw_recexpr -> Sexplib0.Sexp.t
Sourceval _t_to_yojson : _t -> Yojson.Safe.t
Sourceval _t_of_yojson : Yojson.Safe.t -> _t Ppx_deriving_yojson_runtime.error_or
Sourceval raw_tacexpr_to_yojson : raw_tacexpr -> Yojson.Safe.t
Sourceval raw_tacexpr_of_yojson : Yojson.Safe.t -> raw_tacexpr Ppx_deriving_yojson_runtime.error_or
Sourceval raw_taccase_to_yojson : raw_taccase -> Yojson.Safe.t
Sourceval raw_taccase_of_yojson : Yojson.Safe.t -> raw_taccase Ppx_deriving_yojson_runtime.error_or
Sourceval raw_recexpr_to_yojson : raw_recexpr -> Yojson.Safe.t
Sourceval raw_recexpr_of_yojson : Yojson.Safe.t -> raw_recexpr Ppx_deriving_yojson_runtime.error_or
Sourceval _ : Yojson.Safe.t -> raw_recexpr Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold__t : _t Base__Ppx_hash_lib.hash_fold
Sourceval hash_fold_raw_tacexpr : raw_tacexpr Base__Hash.folder
Sourceval hash_fold_raw_taccase : raw_taccase Base__Hash.folder
Sourceval hash_fold_raw_recexpr : Ppx_hash_lib.Std.Hash.state -> raw_recexpr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash__t : _t -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_raw_tacexpr : raw_tacexpr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_raw_taccase : raw_taccase -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_raw_recexpr : raw_recexpr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare__t : _t -> _t -> int
Sourceval compare_raw_tacexpr : raw_tacexpr -> raw_tacexpr -> int
Sourceval compare_raw_taccase : raw_taccase -> raw_taccase -> int
Sourceval 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