Skip to content

Commit e4d5676

Browse files
committed
Adapt to rocq-prover/rocq#21450 (Add poly flag to declare_projections)
1 parent c8c1464 commit e4d5676

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/lean.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1373,9 +1373,10 @@ and declare_ind { name = n; params; ty; ctors; univs } i =
13731373
fields
13741374
in
13751375
let implfs = List.map (fun _ -> []) fields in
1376+
let poly = PolyFlags.default in
13761377
ignore
13771378
(Record.Internal.declare_projections (mind, 0) ~kind ~inhabitant_id
1378-
proj_flags implfs)
1379+
proj_flags ~poly implfs)
13791380
| _ -> ()
13801381
in
13811382
(mind, algs, ind_name, cnames, univs, squashy)

0 commit comments

Comments
 (0)