Skip to content

Commit e1c1ad7

Browse files
authored
Merge pull request ejgallego#1019 from SkySkimmer/mip-mind-record
Adapt to rocq-prover/rocq#21069 (records can be mutual with non records)
2 parents ed270b0 + 0229b93 commit e1c1ad7

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

serlib/ser_declarations.ml

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,10 @@ type squash_info =
5656
[%import: Declarations.squash_info]
5757
[@@deriving sexp,yojson,hash,compare]
5858

59+
type record_info =
60+
[%import: Declarations.record_info]
61+
[@@deriving sexp,yojson,hash,compare]
62+
5963
type one_inductive_body =
6064
[%import: Declarations.one_inductive_body]
6165
[@@deriving sexp,yojson,hash,compare]
@@ -126,10 +130,6 @@ type recursivity_kind =
126130
[%import: Declarations.recursivity_kind]
127131
[@@deriving sexp,yojson,hash,compare]
128132

129-
type record_info =
130-
[%import: Declarations.record_info]
131-
[@@deriving sexp,yojson,hash,compare]
132-
133133
type template_universes =
134134
[%import: Declarations.template_universes]
135135
[@@deriving sexp,yojson,hash,compare]

0 commit comments

Comments
 (0)