Skip to content

Adapt to rocq-prover/rocq#21450 (Add poly flag to declare_projections) #56

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
TDiazT wants to merge 1 commit into from
Closed

Adapt to rocq-prover/rocq#21450 (Add poly flag to declare_projections) #56

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion src/lean.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1373,9 +1373,10 @@ and declare_ind { name = n; params; ty; ctors; univs } i =
fields
in
let implfs = List.map (fun _ -> []) fields in
let poly = PolyFlags.default in
ignore
(Record.Internal.declare_projections (mind, 0) ~kind ~inhabitant_id
proj_flags implfs)
proj_flags ~poly implfs)
Copy link
Collaborator

@SkySkimmer SkySkimmer Jan 19, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

IIUC the poly argument is ignored for primitive records
If that's correct please add a comment about it
(poly = default is incorrect otherwise as we should be univ poly)

| _ -> ()
in
(mind, algs, ind_name, cnames, univs, squashy)
Expand Down