From c745b4e70f53337ef38bcbb2cdd78ca8b11135fc Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 28 Nov 2024 14:54:19 +0100 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530 --- theories/Type/Constants.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Type/Constants.v b/theories/Type/Constants.v index b0f2d285..94a49472 100644 --- a/theories/Type/Constants.v +++ b/theories/Type/Constants.v @@ -37,8 +37,8 @@ Register Logic.Empty as equations.bottom.type. Register Logic.Empty_case as equations.bottom.case. Register Logic.Empty_rect as equations.bottom.elim. -Register Stdlib.Init.Datatypes.unit as equations.top.type. -Register Stdlib.Init.Datatypes.tt as equations.top.intro. +Register Corelib.Init.Datatypes.unit as equations.top.type. +Register Corelib.Init.Datatypes.tt as equations.top.intro. Register Equations.Type.Logic.unit_rect as equations.top.elim. Register Logic.prod as equations.conj.type.