stdpp constrains the template universe option.u0
The file fin_maps.v
is incompatible with any Coq code that uses Some id
, due to universe constraints:
Definition x := Some id.
From stdpp Require Import fin_maps.
(*
Error: Universe inconsistency. Cannot enforce option.u0 <= base.Equiv.u0 because base.Equiv.u0
<= Coq.Relations.Relation_Definitions.1 <= ID.u0 < option.u0.
*)
Another way to see the problem is the following:
From stdpp Require Import fin_maps.
Constraint ID.u0 <= option.u0.
(*
Error: Universe inconsistency. Cannot enforce ID.u0 <= option.u0 because option.u0 <= MapFold.u2
< Coq.Relations.Relation_Definitions.1 <= ID.u0.
*)
This was diagnosed on the Coq Zulip with help from Gaëtan Gilbert.