summaryrefslogtreecommitdiff
path: root/cfrontend/Cstrategy.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Cstrategy.v')
-rw-r--r--cfrontend/Cstrategy.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 0d2f235..b28409d 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -15,7 +15,6 @@
(** A deterministic evaluation strategy for C. *)
-Require Import Coq.Program.Equality.
Require Import Axioms.
Require Import Coqlib.
Require Import Errors.