Skip to content

Commit 1372656

Browse files
authored
Merge pull request #41 from SkySkimmer/mip-mind-record
Adapt to rocq-prover/rocq#21069 (records can be mutual with non records)
2 parents d64fc71 + 1db7b45 commit 1372656

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

src/lean.ml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1142,9 +1142,9 @@ let rec to_constr =
11421142
let ((ind, _) as indu) =
11431143
Constr.destInd (EConstr.Unsafe.to_constr tc)
11441144
in
1145-
let mib = Global.lookup_mind (fst ind) in
1145+
let mib, mip = Inductive.lookup_mind_specif (Global.env()) ind in
11461146
begin
1147-
match mib.mind_record with
1147+
match mip.mind_record with
11481148
| PrimRecord infos ->
11491149
let p, r =
11501150
Declareops.inductive_make_projection ind mib ~proj_arg:field
@@ -1153,7 +1153,7 @@ let rec to_constr =
11531153
mkProj (Projection.make p false, r, c)
11541154
| NotRecord | FakeRecord ->
11551155
if
1156-
mib.mind_packets.(snd ind).mind_relevance
1156+
mip.mind_relevance
11571157
== EConstr.Unsafe.to_relevance EConstr.ERelevance.irrelevant
11581158
then
11591159
CErrors.user_err

0 commit comments

Comments
 (0)