Skip to content

Adapt to https://github.com/rocq-prover/rocq/pull/21851 #588

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

Merged
proux01 merged 1 commit into from
Apr 2, 2026
Merged

Adapt to https://github.com/rocq-prover/rocq/pull/21851 #588

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
22 changes: 11 additions & 11 deletions HB/structures.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,19 +27,19 @@ Register id_phant as hb.id.
Register id_phant_disabled as hb.id_disabled.
Register ignore as hb.ignore.
Register ignore_disabled as hb.ignore_disabled.
Register Coq.Init.Datatypes.None as hb.none.
Register Corelib.Init.Datatypes.None as hb.none.
Register nomsg as hb.nomsg.
Register is_not_canonically_a as hb.not_a_msg.
Register Coq.Init.Datatypes.Some as hb.some.
Register Coq.Init.Datatypes.pair as hb.pair.
Register Coq.Init.Datatypes.prod as hb.prod.
Register Coq.Init.Specif.sigT as hb.sigT.
Register Coq.ssr.ssreflect.phant as hb.phant.
Register Coq.ssr.ssreflect.Phant as hb.Phant.
Register Coq.ssr.ssreflect.phantom as hb.phantom.
Register Coq.ssr.ssreflect.Phantom as hb.Phantom.
Register Coq.Init.Logic.eq as hb.eq.
Register Coq.Init.Logic.eq_refl as hb.erefl.
Register Corelib.Init.Datatypes.Some as hb.some.
Register Corelib.Init.Datatypes.pair as hb.pair.
Register Corelib.Init.Datatypes.prod as hb.prod.
Register Corelib.Init.Specif.sigT as hb.sigT.
Register Corelib.ssr.ssreflect.phant as hb.phant.
Register Corelib.ssr.ssreflect.Phant as hb.Phant.
Register Corelib.ssr.ssreflect.phantom as hb.phantom.
Register Corelib.ssr.ssreflect.Phantom as hb.Phantom.
Register Corelib.Init.Logic.eq as hb.eq.
Register Corelib.Init.Logic.eq_refl as hb.erefl.
Register new as hb.new.
Register eta as hb.eta.

Expand Down
Loading