package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.2.0.8.17.tbz
sha256=36340f464107ac60bb4033fad249984690cdcce3a6bef4ca439ffb2a4458dbf9
sha512=4866f4c2f0acda0c114e27b32cd60fa054333e1c7249227b8c3b23a316d7f306676203bd317f135a40368a292b7b49b76f0bdacff21d7e9bfb5a422d1c8d6ad8
doc/src/serlib_ltac2/ser_tac2expr.ml.html
Source file ser_tac2expr.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174open Serlib module Loc = Ser_loc module CAst = Ser_cAst module Names = Ser_names module Libnames = Ser_libnames open Sexplib.Std open Ppx_hash_lib.Std.Hash.Builtin open Ppx_compare_lib.Builtin let hash_fold_array = hash_fold_array_frozen type mutable_flag = [%import: Ltac2_plugin.Tac2expr.mutable_flag] [@@deriving sexp,yojson,hash,compare] type uid = [%import: Ltac2_plugin.Tac2expr.uid] [@@deriving sexp,yojson,hash,compare] type lid = [%import: Ltac2_plugin.Tac2expr.lid] [@@deriving sexp,yojson,hash,compare] type rec_flag = [%import: Ltac2_plugin.Tac2expr.rec_flag] [@@deriving sexp,yojson,hash,compare] type redef_flag = [%import: Ltac2_plugin.Tac2expr.redef_flag] [@@deriving sexp,yojson,hash,compare] type 'a or_relid = [%import: 'a Ltac2_plugin.Tac2expr.or_relid] [@@deriving sexp,yojson,hash,compare] type 'a or_tuple = [%import: 'a Ltac2_plugin.Tac2expr.or_tuple] [@@deriving sexp,yojson,hash,compare] type type_constant = [%import: Ltac2_plugin.Tac2expr.type_constant] [@@deriving sexp,yojson,hash,compare] type raw_typexpr_r = [%import: Ltac2_plugin.Tac2expr.raw_typexpr_r] [@@deriving sexp,yojson,hash,compare] and raw_typexpr = [%import: Ltac2_plugin.Tac2expr.raw_typexpr] [@@deriving sexp,yojson,hash,compare] type raw_typedef = [%import: Ltac2_plugin.Tac2expr.raw_typedef] [@@deriving sexp,yojson,hash,compare] type raw_quant_typedef = [%import: Ltac2_plugin.Tac2expr.raw_quant_typedef] [@@deriving sexp,yojson,hash,compare] type atom = [%import: Ltac2_plugin.Tac2expr.atom] [@@deriving sexp,yojson,hash,compare] type ltac_constant = [%import: Ltac2_plugin.Tac2expr.ltac_constant] [@@deriving sexp,yojson,hash,compare] type ltac_alias = [%import: Ltac2_plugin.Tac2expr.ltac_alias] [@@deriving sexp,yojson,hash,compare] type ltac_constructor = [%import: Ltac2_plugin.Tac2expr.ltac_constructor] [@@deriving sexp,yojson,hash,compare] type ltac_projection = [%import: Ltac2_plugin.Tac2expr.ltac_projection] [@@deriving sexp,yojson,hash,compare] type raw_patexpr = [%import: Ltac2_plugin.Tac2expr.raw_patexpr] [@@deriving sexp,yojson,hash,compare] and raw_patexpr_r = [%import: Ltac2_plugin.Tac2expr.raw_patexpr_r] [@@deriving sexp,yojson,hash,compare] type tacref = [%import: Ltac2_plugin.Tac2expr.tacref] [@@deriving sexp,yojson,hash,compare] module ObjS = struct type t = Obj.t let name = "Obj.t" end module Obj = SerType.Opaque(ObjS) module T2ESpec = struct type t = Ltac2_plugin.Tac2expr.raw_tacexpr_r open Ltac2_plugin.Tac2expr type _t = | CTacAtm of atom | CTacRef of tacref or_relid | CTacCst of ltac_constructor or_tuple or_relid | CTacFun of raw_patexpr list * raw_tacexpr | CTacApp of raw_tacexpr * raw_tacexpr list | CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr | CTacCnv of raw_tacexpr * raw_typexpr | CTacSeq of raw_tacexpr * raw_tacexpr | CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr | CTacCse of raw_tacexpr * raw_taccase list | CTacRec of raw_recexpr | CTacPrj of raw_tacexpr * ltac_projection or_relid | CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr | CTacExt of int * Obj.t and raw_tacexpr = _t CAst.t and raw_taccase = [%import: Ltac2_plugin.Tac2expr.raw_taccase] and raw_recexpr = [%import: Ltac2_plugin.Tac2expr.raw_recexpr] [@@deriving sexp,yojson,hash,compare] end module T2E = Serlib.SerType.Pierce(T2ESpec) type raw_tacexpr_r = T2E.t [@@deriving sexp,yojson,hash,compare] type raw_tacexpr = [%import: Ltac2_plugin.Tac2expr.raw_tacexpr] [@@deriving sexp,yojson,hash,compare] type ml_tactic_name = [%import: Ltac2_plugin.Tac2expr.ml_tactic_name] [@@deriving sexp,yojson,hash,compare] type sexpr = [%import: Ltac2_plugin.Tac2expr.sexpr] [@@deriving sexp,yojson,hash,compare] type strexpr = [%import: Ltac2_plugin.Tac2expr.strexpr] [@@deriving sexp,yojson,hash,compare] type case_info = [%import: Ltac2_plugin.Tac2expr.case_info] [@@deriving sexp,yojson,hash,compare] type 'a open_match = [%import: 'a Ltac2_plugin.Tac2expr.open_match] [@@deriving sexp,yojson,hash,compare] module GT2ESpec = struct type t = Ltac2_plugin.Tac2expr.glb_tacexpr open Ltac2_plugin.Tac2expr type _t = | GTacAtm of atom | GTacVar of Names.Id.t | GTacRef of ltac_constant | GTacFun of Names.Name.t list * _t | GTacApp of _t * _t list | GTacLet of rec_flag * (Names.Name.t * _t) list * _t | GTacCst of case_info * int * _t list | GTacCse of _t * case_info * _t array * (Names.Name.t array * _t) array | GTacPrj of type_constant * _t * int | GTacSet of type_constant * _t * int * _t | GTacOpn of ltac_constructor * _t list | GTacWth of _t open_match | GTacExt of int * Obj.t | GTacPrm of ml_tactic_name * _t list [@@deriving sexp,yojson,hash,compare] end module GT2E = Serlib.SerType.Pierce(GT2ESpec) type glb_tacexpr = GT2E.t [@@deriving sexp,yojson,hash,compare]