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.