Fixed universe inconsistencies.

weakmemory · Oct 23, 2023 · 63f2a13 · 63f2a13
1 parent da203b7
commit 63f2a13
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 1 deletion.
diff --git a/src/itree/ITreeLang.v b/src/itree/ITreeLang.v
@@ -35,9 +35,9 @@ From PromisingLib Require Import Event.
 Require Export ITreeLib.
 Require Export Program.
 
+Set Universe Polymorphism.
 Set Implicit Arguments.
 
-
 Module MemE.
   Variant rmw :=
   | fetch_add (addendum:Const.t)

diff --git a/src/model/Configuration.v b/src/model/Configuration.v
@@ -20,6 +20,7 @@ Require Import Global.
 Require Import Local.
 Require Import Thread.
 
+Set Universe Polymorphism.
 Set Implicit Arguments.
 
 

diff --git a/src/trans/Compatibility.v b/src/trans/Compatibility.v
@@ -33,6 +33,7 @@ Require Import SimMemory.
 Require Import SimGlobal.
 Require Import SimThread.
 
+Set Universe Polymorphism.
 Set Implicit Arguments.