Module `Serlib_ltac2.Ser_tac2expr`Source

module Loc = Serlib.Ser_loc

module CAst = Serlib.Ser_cAst

module Names = Serlib.Ser_names

module Libnames = Serlib.Ser_libnames

Sourceval hash_fold_array : 'a Base__Hash.folder -> 'a array Base__Hash.folder

Sourcetype mutable_flag = bool

Sourceval mutable_flag_of_sexp : Sexplib0.Sexp.t -> mutable_flag

Sourceval sexp_of_mutable_flag : mutable_flag -> Sexplib0.Sexp.t

Sourceval mutable_flag_to_yojson : mutable_flag -> Yojson.Safe.t

Source

val mutable_flag_of_yojson : 
  Yojson.Safe.t ->
  mutable_flag Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_mutable_flag : 
  Ppx_hash_lib.Std.Hash.state ->
  mutable_flag ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_mutable_flag : mutable_flag -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_mutable_flag : mutable_flag -> mutable_flag -> int

Sourcetype uid = Names.Id.t

Sourceval uid_of_sexp : Sexplib0.Sexp.t -> uid

Sourceval sexp_of_uid : uid -> Sexplib0.Sexp.t

Sourceval uid_to_yojson : uid -> Yojson.Safe.t

Sourceval uid_of_yojson : Yojson.Safe.t -> uid Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_uid : 
  Ppx_hash_lib.Std.Hash.state ->
  uid ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_uid : uid -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_uid : uid -> uid -> int

Sourcetype lid = Names.Id.t

Sourceval lid_of_sexp : Sexplib0.Sexp.t -> lid

Sourceval sexp_of_lid : lid -> Sexplib0.Sexp.t

Sourceval lid_to_yojson : lid -> Yojson.Safe.t

Sourceval lid_of_yojson : Yojson.Safe.t -> lid Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_lid : 
  Ppx_hash_lib.Std.Hash.state ->
  lid ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_lid : lid -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_lid : lid -> lid -> int

Sourcetype rec_flag = bool

Sourceval rec_flag_of_sexp : Sexplib0.Sexp.t -> rec_flag

Sourceval sexp_of_rec_flag : rec_flag -> Sexplib0.Sexp.t

Sourceval rec_flag_to_yojson : rec_flag -> Yojson.Safe.t

Source

val rec_flag_of_yojson : 
  Yojson.Safe.t ->
  rec_flag Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_rec_flag : 
  Ppx_hash_lib.Std.Hash.state ->
  rec_flag ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_rec_flag : rec_flag -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_rec_flag : rec_flag -> rec_flag -> int

Sourcetype redef_flag = bool

Sourceval redef_flag_of_sexp : Sexplib0.Sexp.t -> redef_flag

Sourceval sexp_of_redef_flag : redef_flag -> Sexplib0.Sexp.t

Sourceval redef_flag_to_yojson : redef_flag -> Yojson.Safe.t

Source

val redef_flag_of_yojson : 
  Yojson.Safe.t ->
  redef_flag Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_redef_flag : 
  Ppx_hash_lib.Std.Hash.state ->
  redef_flag ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_redef_flag : redef_flag -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_redef_flag : redef_flag -> redef_flag -> int

Sourcetype 'a or_relid = 'a Ltac2_plugin.Tac2expr.or_relid =

| RelId of Libnames.qualid
| AbsKn of 'a

Source

val or_relid_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a or_relid

Source

val sexp_of_or_relid : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a or_relid ->
  Sexplib0.Sexp.t

Source

val or_relid_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a or_relid ->
  Yojson.Safe.t

Source

val or_relid_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a or_relid Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_or_relid : 
  'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
  Ppx_hash_lib.Std.Hash.state ->
  'a or_relid ->
  Ppx_hash_lib.Std.Hash.state

Source

val compare_or_relid : 
  'a. ('a -> 'a -> int) ->
  'a or_relid ->
  'a or_relid ->
  int

Sourcetype 'a or_tuple = 'a Ltac2_plugin.Tac2expr.or_tuple =

| Tuple of int
| Other of 'a

Source

val or_tuple_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a or_tuple

Source

val sexp_of_or_tuple : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a or_tuple ->
  Sexplib0.Sexp.t

Source

val or_tuple_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a or_tuple ->
  Yojson.Safe.t

Source

val or_tuple_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a or_tuple Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_or_tuple : 
  'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
  Ppx_hash_lib.Std.Hash.state ->
  'a or_tuple ->
  Ppx_hash_lib.Std.Hash.state

Source

val compare_or_tuple : 
  'a. ('a -> 'a -> int) ->
  'a or_tuple ->
  'a or_tuple ->
  int

Sourcetype type_constant = Names.KerName.t

Sourceval type_constant_of_sexp : Sexplib0.Sexp.t -> type_constant

Sourceval sexp_of_type_constant : type_constant -> Sexplib0.Sexp.t

Sourceval type_constant_to_yojson : type_constant -> Yojson.Safe.t

Source

val type_constant_of_yojson : 
  Yojson.Safe.t ->
  type_constant Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_type_constant : 
  Ppx_hash_lib.Std.Hash.state ->
  type_constant ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_type_constant : type_constant -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_type_constant : type_constant -> type_constant -> int

Sourcetype raw_typexpr_r = Ltac2_plugin.Tac2expr.raw_typexpr_r =

| CTypVar of Names.Name.t
| CTypArrow of raw_typexpr * raw_typexpr
| CTypRef of type_constant or_tuple or_relid * raw_typexpr list

Sourceand raw_typexpr = raw_typexpr_r CAst.t

Sourceval raw_typexpr_r_of_sexp : Sexplib0__.Sexp.t -> raw_typexpr_r

Sourceval raw_typexpr_of_sexp : Sexplib0__.Sexp.t -> raw_typexpr

Sourceval sexp_of_raw_typexpr_r : raw_typexpr_r -> Sexplib0__.Sexp.t

Sourceval sexp_of_raw_typexpr : raw_typexpr -> Sexplib0__.Sexp.t

Sourceval raw_typexpr_r_to_yojson : raw_typexpr_r -> Yojson.Safe.t

Source

val raw_typexpr_r_of_yojson : 
  Yojson.Safe.t ->
  raw_typexpr_r Ppx_deriving_yojson_runtime.error_or

Sourceval raw_typexpr_to_yojson : raw_typexpr -> Yojson.Safe.t

Source

val raw_typexpr_of_yojson : 
  Yojson.Safe.t ->
  raw_typexpr Ppx_deriving_yojson_runtime.error_or

Sourceval hash_fold_raw_typexpr_r : raw_typexpr_r Base__Ppx_hash_lib.hash_fold

Sourceval hash_fold_raw_typexpr : raw_typexpr Base__Hash.folder

Sourceval hash_raw_typexpr_r : raw_typexpr_r -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval hash_raw_typexpr : raw_typexpr -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_raw_typexpr_r : raw_typexpr_r -> raw_typexpr_r -> int

Sourceval compare_raw_typexpr : raw_typexpr -> raw_typexpr -> int

Sourcetype raw_typedef = Ltac2_plugin.Tac2expr.raw_typedef =

| CTydDef of raw_typexpr option
| CTydAlg of (uid * raw_typexpr list) list
| CTydRec of (lid * mutable_flag * raw_typexpr) list
| CTydOpn

Sourceval raw_typedef_of_sexp : Sexplib0.Sexp.t -> raw_typedef

Sourceval sexp_of_raw_typedef : raw_typedef -> Sexplib0.Sexp.t

Sourceval raw_typedef_to_yojson : raw_typedef -> Yojson.Safe.t

Source

val raw_typedef_of_yojson : 
  Yojson.Safe.t ->
  raw_typedef Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_raw_typedef : 
  Ppx_hash_lib.Std.Hash.state ->
  raw_typedef ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_raw_typedef : raw_typedef -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_raw_typedef : raw_typedef -> raw_typedef -> int

Sourcetype raw_quant_typedef = Names.lident list * raw_typedef

Sourceval raw_quant_typedef_of_sexp : Sexplib0.Sexp.t -> raw_quant_typedef

Sourceval sexp_of_raw_quant_typedef : raw_quant_typedef -> Sexplib0.Sexp.t

Sourceval raw_quant_typedef_to_yojson : raw_quant_typedef -> Yojson.Safe.t

Source

val raw_quant_typedef_of_yojson : 
  Yojson.Safe.t ->
  raw_quant_typedef Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_raw_quant_typedef : 
  Ppx_hash_lib.Std.Hash.state ->
  raw_quant_typedef ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_raw_quant_typedef : 
  raw_quant_typedef ->
  Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_raw_quant_typedef : raw_quant_typedef -> raw_quant_typedef -> int

Sourcetype 'a glb_typexpr = 'a Ltac2_plugin.Tac2expr.glb_typexpr =

| GTypVar of 'a
| GTypArrow of 'a glb_typexpr * 'a glb_typexpr
| GTypRef of type_constant or_tuple * 'a glb_typexpr list

Source

val glb_typexpr_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a glb_typexpr

Source

val sexp_of_glb_typexpr : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a glb_typexpr ->
  Sexplib0.Sexp.t

Source

val glb_typexpr_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a glb_typexpr ->
  Yojson.Safe.t

Source

val glb_typexpr_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a glb_typexpr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_glb_typexpr : 
  'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
  Ppx_hash_lib.Std.Hash.state ->
  'a glb_typexpr ->
  Ppx_hash_lib.Std.Hash.state

Source

val compare_glb_typexpr : 
  'a. ('a -> 'a -> int) ->
  'a glb_typexpr ->
  'a glb_typexpr ->
  int

Sourcetype atom = Ltac2_plugin.Tac2expr.atom =

| AtmInt of int
| AtmStr of string

Sourceval atom_of_sexp : Sexplib0.Sexp.t -> atom

Sourceval sexp_of_atom : atom -> Sexplib0.Sexp.t

Sourceval atom_to_yojson : atom -> Yojson.Safe.t

Sourceval atom_of_yojson : Yojson.Safe.t -> atom Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_atom : 
  Ppx_hash_lib.Std.Hash.state ->
  atom ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_atom : atom -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_atom : atom -> atom -> int

Sourcetype ltac_constant = Names.KerName.t

Sourceval ltac_constant_of_sexp : Sexplib0.Sexp.t -> ltac_constant

Sourceval sexp_of_ltac_constant : ltac_constant -> Sexplib0.Sexp.t

Sourceval ltac_constant_to_yojson : ltac_constant -> Yojson.Safe.t

Source

val ltac_constant_of_yojson : 
  Yojson.Safe.t ->
  ltac_constant Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_ltac_constant : 
  Ppx_hash_lib.Std.Hash.state ->
  ltac_constant ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_ltac_constant : ltac_constant -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_ltac_constant : ltac_constant -> ltac_constant -> int

Sourcetype ltac_alias = Names.KerName.t

Sourceval ltac_alias_of_sexp : Sexplib0.Sexp.t -> ltac_alias

Sourceval sexp_of_ltac_alias : ltac_alias -> Sexplib0.Sexp.t

Sourceval ltac_alias_to_yojson : ltac_alias -> Yojson.Safe.t

Source

val ltac_alias_of_yojson : 
  Yojson.Safe.t ->
  ltac_alias Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_ltac_alias : 
  Ppx_hash_lib.Std.Hash.state ->
  ltac_alias ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_ltac_alias : ltac_alias -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_ltac_alias : ltac_alias -> ltac_alias -> int

Sourcetype ltac_constructor = Names.KerName.t

Sourceval ltac_constructor_of_sexp : Sexplib0.Sexp.t -> ltac_constructor

Sourceval sexp_of_ltac_constructor : ltac_constructor -> Sexplib0.Sexp.t

Sourceval ltac_constructor_to_yojson : ltac_constructor -> Yojson.Safe.t

Source

val ltac_constructor_of_yojson : 
  Yojson.Safe.t ->
  ltac_constructor Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_ltac_constructor : 
  Ppx_hash_lib.Std.Hash.state ->
  ltac_constructor ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_ltac_constructor : 
  ltac_constructor ->
  Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_ltac_constructor : ltac_constructor -> ltac_constructor -> int

Sourcetype ltac_projection = Names.KerName.t

Sourceval ltac_projection_of_sexp : Sexplib0.Sexp.t -> ltac_projection

Sourceval sexp_of_ltac_projection : ltac_projection -> Sexplib0.Sexp.t

Sourceval ltac_projection_to_yojson : ltac_projection -> Yojson.Safe.t

Source

val ltac_projection_of_yojson : 
  Yojson.Safe.t ->
  ltac_projection Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_ltac_projection : 
  Ppx_hash_lib.Std.Hash.state ->
  ltac_projection ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_ltac_projection : ltac_projection -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_ltac_projection : ltac_projection -> ltac_projection -> int

Sourcetype raw_patexpr = raw_patexpr_r CAst.t

Sourceand raw_patexpr_r = Ltac2_plugin.Tac2expr.raw_patexpr_r =

| CPatVar of Names.Name.t
| CPatAtm of atom
| CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
| CPatRecord of (ltac_projection or_relid * raw_patexpr) list
| CPatCnv of raw_patexpr * raw_typexpr
| CPatOr of raw_patexpr list
| CPatAs of raw_patexpr * Names.lident

Sourceval raw_patexpr_of_sexp : Sexplib0__.Sexp.t -> raw_patexpr

Sourceval raw_patexpr_r_of_sexp : Sexplib0__.Sexp.t -> raw_patexpr_r

Sourceval sexp_of_raw_patexpr : raw_patexpr -> Sexplib0__.Sexp.t

Sourceval sexp_of_raw_patexpr_r : raw_patexpr_r -> Sexplib0__.Sexp.t

Sourceval raw_patexpr_to_yojson : raw_patexpr -> Yojson.Safe.t

Source

val raw_patexpr_of_yojson : 
  Yojson.Safe.t ->
  raw_patexpr Ppx_deriving_yojson_runtime.error_or

Sourceval raw_patexpr_r_to_yojson : raw_patexpr_r -> Yojson.Safe.t

Source

val raw_patexpr_r_of_yojson : 
  Yojson.Safe.t ->
  raw_patexpr_r Ppx_deriving_yojson_runtime.error_or

Sourceval hash_fold_raw_patexpr : raw_patexpr Base__Hash.folder

Sourceval hash_fold_raw_patexpr_r : raw_patexpr_r Base__Ppx_hash_lib.hash_fold

Sourceval hash_raw_patexpr : raw_patexpr -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval hash_raw_patexpr_r : raw_patexpr_r -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_raw_patexpr : raw_patexpr -> raw_patexpr -> int

Sourceval compare_raw_patexpr_r : raw_patexpr_r -> raw_patexpr_r -> int

Sourcetype tacref = Ltac2_plugin.Tac2expr.tacref =

| TacConstant of ltac_constant
| TacAlias of ltac_alias

Sourceval tacref_of_sexp : Sexplib0.Sexp.t -> tacref

Sourceval sexp_of_tacref : tacref -> Sexplib0.Sexp.t

Sourceval tacref_to_yojson : tacref -> Yojson.Safe.t

Source

val tacref_of_yojson : 
  Yojson.Safe.t ->
  tacref Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_tacref : 
  Ppx_hash_lib.Std.Hash.state ->
  tacref ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_tacref : tacref -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_tacref : tacref -> tacref -> int

Sourcetype ml_tactic_name = Ltac2_plugin.Tac2expr.ml_tactic_name = {

mltac_plugin : string;
mltac_tactic : string;

}

Sourceval ml_tactic_name_of_sexp : Sexplib0.Sexp.t -> ml_tactic_name

Sourceval sexp_of_ml_tactic_name : ml_tactic_name -> Sexplib0.Sexp.t

Sourceval ml_tactic_name_to_yojson : ml_tactic_name -> Yojson.Safe.t

Source

val ml_tactic_name_of_yojson : 
  Yojson.Safe.t ->
  ml_tactic_name Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_ml_tactic_name : 
  Ppx_hash_lib.Std.Hash.state ->
  ml_tactic_name ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_ml_tactic_name : ml_tactic_name -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_ml_tactic_name : ml_tactic_name -> ml_tactic_name -> int

Sourcetype sexpr = Ltac2_plugin.Tac2expr.sexpr =

| SexprStr of string CAst.t
| SexprInt of int CAst.t
| SexprRec of Loc.t * Names.Id.t option CAst.t * sexpr list

Sourceval sexpr_of_sexp : Sexplib0__.Sexp.t -> sexpr

Sourceval sexp_of_sexpr : sexpr -> Sexplib0__.Sexp.t

Sourceval sexpr_to_yojson : sexpr -> Yojson.Safe.t

Source

val sexpr_of_yojson : 
  Yojson.Safe.t ->
  sexpr Ppx_deriving_yojson_runtime.error_or

Sourceval hash_fold_sexpr : sexpr Base__Hash.folder

Sourceval hash_sexpr : sexpr -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_sexpr : sexpr -> sexpr -> int

Sourcetype ctor_indx = Ltac2_plugin.Tac2expr.ctor_indx =

| Closed of int
| Open of ltac_constructor

Sourceval ctor_indx_of_sexp : Sexplib0.Sexp.t -> ctor_indx

Sourceval sexp_of_ctor_indx : ctor_indx -> Sexplib0.Sexp.t

Sourceval ctor_indx_to_yojson : ctor_indx -> Yojson.Safe.t

Source

val ctor_indx_of_yojson : 
  Yojson.Safe.t ->
  ctor_indx Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_ctor_indx : 
  Ppx_hash_lib.Std.Hash.state ->
  ctor_indx ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_ctor_indx : ctor_indx -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_ctor_indx : ctor_indx -> ctor_indx -> int

Sourcetype ctor_data_for_patterns = Ltac2_plugin.Tac2expr.ctor_data_for_patterns = {

ctyp : type_constant option;
cnargs : int;
cindx : ctor_indx;

}

Sourceval ctor_data_for_patterns_of_sexp : Sexplib0.Sexp.t -> ctor_data_for_patterns

Sourceval sexp_of_ctor_data_for_patterns : ctor_data_for_patterns -> Sexplib0.Sexp.t

Sourceval ctor_data_for_patterns_to_yojson : ctor_data_for_patterns -> Yojson.Safe.t

Source

val ctor_data_for_patterns_of_yojson : 
  Yojson.Safe.t ->
  ctor_data_for_patterns Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_ctor_data_for_patterns : 
  Ppx_hash_lib.Std.Hash.state ->
  ctor_data_for_patterns ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_ctor_data_for_patterns : 
  ctor_data_for_patterns ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_ctor_data_for_patterns : 
  ctor_data_for_patterns ->
  ctor_data_for_patterns ->
  int

Sourcetype glb_pat = Ltac2_plugin.Tac2expr.glb_pat =

| GPatVar of Names.Name.t
| GPatAtm of atom
| GPatRef of ctor_data_for_patterns * glb_pat list
| GPatOr of glb_pat list
| GPatAs of glb_pat * Names.Id.t

Sourceval glb_pat_of_sexp : Sexplib0__.Sexp.t -> glb_pat

Sourceval sexp_of_glb_pat : glb_pat -> Sexplib0__.Sexp.t

Sourceval glb_pat_to_yojson : glb_pat -> Yojson.Safe.t

Source

val glb_pat_of_yojson : 
  Yojson.Safe.t ->
  glb_pat Ppx_deriving_yojson_runtime.error_or

Sourceval hash_fold_glb_pat : glb_pat Base__Hash.folder

Sourceval hash_glb_pat : glb_pat -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_glb_pat : glb_pat -> glb_pat -> int

Sourcetype case_info = type_constant or_tuple

Sourceval case_info_of_sexp : Sexplib0.Sexp.t -> case_info

Sourceval sexp_of_case_info : case_info -> Sexplib0.Sexp.t

Sourceval case_info_to_yojson : case_info -> Yojson.Safe.t

Source

val case_info_of_yojson : 
  Yojson.Safe.t ->
  case_info Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_case_info : 
  Ppx_hash_lib.Std.Hash.state ->
  case_info ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_case_info : case_info -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_case_info : case_info -> case_info -> int

Sourcetype 'a open_match = 'a Ltac2_plugin.Tac2expr.open_match = {

opn_match : 'a;
opn_branch : (Names.Name.t * Names.Name.t array * 'a) Names.KNmap.t;
opn_default : Names.Name.t * 'a;

}

Source

val open_match_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a open_match

Source

val sexp_of_open_match : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a open_match ->
  Sexplib0.Sexp.t

Source

val open_match_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a open_match ->
  Yojson.Safe.t

Source

val open_match_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a open_match Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_open_match : 
  'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
  Ppx_hash_lib.Std.Hash.state ->
  'a open_match ->
  Ppx_hash_lib.Std.Hash.state

Source

val compare_open_match : 
  'a. ('a -> 'a -> int) ->
  'a open_match ->
  'a open_match ->
  int

Sourcemodule ObjS : sig ... end

module Obj : sig ... end

Sourcemodule GT2ESpec : sig ... end

module GT2E : sig ... end

Sourcetype glb_tacexpr = GT2E.t

Sourceval glb_tacexpr_of_sexp : Sexplib0.Sexp.t -> glb_tacexpr

Sourceval sexp_of_glb_tacexpr : glb_tacexpr -> Sexplib0.Sexp.t

Sourceval glb_tacexpr_to_yojson : glb_tacexpr -> Yojson.Safe.t

Source

val glb_tacexpr_of_yojson : 
  Yojson.Safe.t ->
  glb_tacexpr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_glb_tacexpr : 
  Ppx_hash_lib.Std.Hash.state ->
  glb_tacexpr ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_glb_tacexpr : glb_tacexpr -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_glb_tacexpr : glb_tacexpr -> glb_tacexpr -> int

Sourcemodule T2ESpec : sig ... end

module T2E : sig ... end

Sourcetype raw_tacexpr_r = T2E.t

Sourceval raw_tacexpr_r_of_sexp : Sexplib0.Sexp.t -> raw_tacexpr_r

Sourceval sexp_of_raw_tacexpr_r : raw_tacexpr_r -> Sexplib0.Sexp.t

Sourceval raw_tacexpr_r_to_yojson : raw_tacexpr_r -> Yojson.Safe.t

Source

val raw_tacexpr_r_of_yojson : 
  Yojson.Safe.t ->
  raw_tacexpr_r Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_raw_tacexpr_r : 
  Ppx_hash_lib.Std.Hash.state ->
  raw_tacexpr_r ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_raw_tacexpr_r : raw_tacexpr_r -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_raw_tacexpr_r : raw_tacexpr_r -> raw_tacexpr_r -> int

Sourcetype raw_tacexpr = raw_tacexpr_r CAst.t

Sourceval raw_tacexpr_of_sexp : Sexplib0.Sexp.t -> raw_tacexpr

Sourceval sexp_of_raw_tacexpr : raw_tacexpr -> Sexplib0.Sexp.t

Sourceval raw_tacexpr_to_yojson : raw_tacexpr -> Yojson.Safe.t

Source

val raw_tacexpr_of_yojson : 
  Yojson.Safe.t ->
  raw_tacexpr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_raw_tacexpr : 
  Ppx_hash_lib.Std.Hash.state ->
  raw_tacexpr ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_raw_tacexpr : raw_tacexpr -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_raw_tacexpr : raw_tacexpr -> raw_tacexpr -> int

Sourcetype strexpr = Ltac2_plugin.Tac2expr.strexpr =

| StrVal of mutable_flag * rec_flag * (Names.lname * raw_tacexpr) list
| StrTyp of rec_flag * (Libnames.qualid * redef_flag * raw_quant_typedef) list
| StrPrm of Names.lident * raw_typexpr * ml_tactic_name
| StrMut of Libnames.qualid * Names.lident option * raw_tacexpr

Sourceval strexpr_of_sexp : Sexplib0.Sexp.t -> strexpr

Sourceval sexp_of_strexpr : strexpr -> Sexplib0.Sexp.t

Sourceval strexpr_to_yojson : strexpr -> Yojson.Safe.t

Source

val strexpr_of_yojson : 
  Yojson.Safe.t ->
  strexpr Ppx_deriving_yojson_runtime.error_or

Sourceval _ : Yojson.Safe.t -> strexpr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_strexpr : 
  Ppx_hash_lib.Std.Hash.state ->
  strexpr ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_strexpr : strexpr -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_strexpr : strexpr -> strexpr -> int

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/serlib_ltac2/Serlib_ltac2/Ser_tac2expr/index.html

Module `Serlib_ltac2.Ser_tac2expr`Source

package coq-lsp

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/serlib_ltac2/Serlib_ltac2/Ser_tac2expr/index.html

Module Serlib_ltac2.Ser_tac2exprSource

dune-project
Dependency

Module `Serlib_ltac2.Ser_tac2expr`Source