diff --git a/HB/structures.v b/HB/structures.v
index 8f47bc83..90fcb358 100644
--- a/HB/structures.v
+++ b/HB/structures.v
@@ -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.