package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.2.3.9.0.tbz
sha256=8776582dddfe768623870cf540ff6ba1e96a44a36e85db18ab93d238d640f92a
sha512=2837889bf99bfe715bd0e752782211a76a14aac71ed37a4fb784f4f0abe338352c9c6d8caa37daf79c036997add1cb306c523f793625b38709f3b5e245380223
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 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203(************************************************************************) (* SerAPI: Coq interaction protocol with bidirectional serialization *) (************************************************************************) (* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) (* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) (* Written by: Emilio J. Gallego Arias and others *) (************************************************************************) open Serlib module Loc = Ser_loc module CAst = Ser_cAst module Names = Ser_names module Libnames = Ser_libnames module Attributes = Ser_attributes 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 'a glb_typexpr = [%import: 'a Ltac2_plugin.Tac2expr.glb_typexpr] [@@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] 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 ctor_indx = [%import: Ltac2_plugin.Tac2expr.ctor_indx] [@@deriving sexp,yojson,hash,compare] type ctor_data_for_patterns = [%import: Ltac2_plugin.Tac2expr.ctor_data_for_patterns] [@@deriving sexp,yojson,hash,compare] type glb_pat = [%import: Ltac2_plugin.Tac2expr.glb_pat] [@@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 ObjS = struct type t = Obj.t let name = "Obj.t" end module Obj = SerType.Opaque(ObjS) 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 | GTacFullMatch of _t * (glb_pat * _t) list | GTacExt of int * Obj.t | GTacPrm of ml_tactic_name [@@deriving sexp,yojson,hash,compare] end module GT2E = Serlib.SerType.Pierce(GT2ESpec) type glb_tacexpr = GT2E.t [@@deriving sexp,yojson,hash,compare] 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 | CTacSyn of (Names.lname * raw_tacexpr) list * Names.KerName.t | 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_tacexpr option * 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 | CTacGlb of int * (Names.lname * raw_tacexpr * int glb_typexpr option) list * glb_tacexpr * int glb_typexpr 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 strexpr = [%import: Ltac2_plugin.Tac2expr.strexpr] [@@deriving sexp,yojson,hash,compare]