summaryrefslogtreecommitdiff
path: root/backend/Tailcallproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Tailcallproof.v')
-rw-r--r--backend/Tailcallproof.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 77725cf..1965b18 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -13,6 +13,7 @@
(** Recognition of tail calls: correctness proof *)
Require Import Coqlib.
+Require Import Compopts.
Require Import Maps.
Require Import AST.
Require Import Integers.