From 4ea7c76d20c40db7685dc89d8c7a4b07fac1da30 Mon Sep 17 00:00:00 2001 From: Bas Spitters Date: Sun, 17 May 2026 16:20:09 +0200 Subject: [PATCH] Map.Interface, Word.Interface: Set Universe Polymorphism MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both files define typeclasses (map, word) that downstream consumers parameterize over. Without [Set Universe Polymorphism], every instance is locked at a fixed universe level, which forces universe-bumping casts at every callsite — and outright blocks composition for downstream code that needs to instantiate at multiple universe levels. Concrete motivation: Jasmin extraction (via the [JasminBridge] in AUCurves) and bedrock2-WP proofs both need to instantiate [map.rep] and [word.rep] at universe levels selected by the surrounding context. With monomorphic interfaces this fails with cryptic 'universe inconsistency' errors that bisect to the interface declaration site. The change is purely a header-level annotation; no proof bodies modified. Verified clean rebuild of the bedrock2 + downstream tree (AUCurves) with no regressions. --- src/coqutil/Map/Interface.v | 1 + src/coqutil/Word/Interface.v | 1 + 2 files changed, 2 insertions(+) diff --git a/src/coqutil/Map/Interface.v b/src/coqutil/Map/Interface.v index 4440dfb2..97537680 100644 --- a/src/coqutil/Map/Interface.v +++ b/src/coqutil/Map/Interface.v @@ -1,3 +1,4 @@ +Set Universe Polymorphism. Require Import coqutil.sanity. Require Import coqutil.Datatypes.HList. Require Import coqutil.Datatypes.List. diff --git a/src/coqutil/Word/Interface.v b/src/coqutil/Word/Interface.v index 13ecbf5f..4b0cbbc8 100644 --- a/src/coqutil/Word/Interface.v +++ b/src/coqutil/Word/Interface.v @@ -1,3 +1,4 @@ +Set Universe Polymorphism. (* Specification of two's complement machine words wrt Z *) Require Import Coq.ZArith.BinIntDef Coq.ZArith.BinInt.