summaryrefslogtreecommitdiff
path: root/common/Determinism.v
diff options
context:
space:
mode:
Diffstat (limited to 'common/Determinism.v')
-rw-r--r--common/Determinism.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/common/Determinism.v b/common/Determinism.v
index d798cf5..26a13ab 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -16,7 +16,6 @@
Require Import Coqlib.
Require Import AST.
Require Import Integers.
-Require Import Values.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.