Skip to content

Commit 5765cbb

Browse files
committed
Adapt to rocq-prover/rocq#19023 (Vernacexpr.subproof_kind)
1 parent fae278e commit 5765cbb

File tree

2 files changed

+8
-0
lines changed

2 files changed

+8
-0
lines changed

serlib/ser_vernacexpr.ml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -281,6 +281,10 @@ type scheme =
281281
[%import: Vernacexpr.scheme]
282282
[@@deriving sexp,yojson,hash,compare]
283283

284+
type subproof_kind =
285+
[%import: Vernacexpr.subproof_kind]
286+
[@@deriving sexp,yojson,hash,compare]
287+
284288
type section_subset_expr =
285289
[%import: Vernacexpr.section_subset_expr]
286290
[@@deriving sexp,yojson,hash,compare]

serlib/ser_vernacexpr.mli

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -204,6 +204,10 @@ type scheme =
204204
[%import: Vernacexpr.scheme]
205205
[@@deriving sexp,yojson,hash,compare]
206206

207+
type subproof_kind =
208+
[%import: Vernacexpr.subproof_kind]
209+
[@@deriving sexp,yojson,hash,compare]
210+
207211
type section_subset_expr =
208212
[%import: Vernacexpr.section_subset_expr]
209213
[@@deriving sexp,yojson,hash,compare]

0 commit comments

Comments
 (0)