Skip to content

Commit

Permalink
Merge pull request #625 from proux01/stdlib_repo
Browse files Browse the repository at this point in the history 
Adapt to coq/coq#19530
  • Loading branch information
@ppedrot
ppedrot authored Dec 6, 2024
2 parents 596d209 + c745b4e commit 3431c88
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions theories/Type/Constants.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Check failure on line 40 in theories/Type/Constants.v

View workflow job for this annotation

GitHub Actions / build (dev, 4.09-flambda, local) 

The reference Corelib.Init.Datatypes.unit was not found in the current

Check failure on line 40 in theories/Type/Constants.v

View workflow job for this annotation

GitHub Actions / build (dev, 4.09-flambda, dune) 

The reference Corelib.Init.Datatypes.unit was not found in the current
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.
Expand Down

0 comments on commit 3431c88

Please sign in to comment.