From 5765cbbb21d3b92ae930d4cb8c62e8b788ea73e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 22 Oct 2024 13:17:07 +0200 Subject: [PATCH] Adapt to coq/coq#19023 (Vernacexpr.subproof_kind) --- serlib/ser_vernacexpr.ml | 4 ++++ serlib/ser_vernacexpr.mli | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/serlib/ser_vernacexpr.ml b/serlib/ser_vernacexpr.ml index 96e422e1..71ee37db 100644 --- a/serlib/ser_vernacexpr.ml +++ b/serlib/ser_vernacexpr.ml @@ -281,6 +281,10 @@ type scheme = [%import: Vernacexpr.scheme] [@@deriving sexp,yojson,hash,compare] +type subproof_kind = + [%import: Vernacexpr.subproof_kind] + [@@deriving sexp,yojson,hash,compare] + type section_subset_expr = [%import: Vernacexpr.section_subset_expr] [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_vernacexpr.mli b/serlib/ser_vernacexpr.mli index 4a94ee65..b1dde167 100644 --- a/serlib/ser_vernacexpr.mli +++ b/serlib/ser_vernacexpr.mli @@ -204,6 +204,10 @@ type scheme = [%import: Vernacexpr.scheme] [@@deriving sexp,yojson,hash,compare] +type subproof_kind = + [%import: Vernacexpr.subproof_kind] + [@@deriving sexp,yojson,hash,compare] + type section_subset_expr = [%import: Vernacexpr.section_subset_expr] [@@deriving sexp,yojson,hash,compare]