aboutsummaryrefslogtreecommitdiffstats
path: root/backend/RTLTunneling.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/RTLTunneling.v')
-rw-r--r--backend/RTLTunneling.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v
index 049160fd..df663f48 100644
--- a/backend/RTLTunneling.v
+++ b/backend/RTLTunneling.v
@@ -19,7 +19,7 @@ Require Import Coqlib Maps Errors.
Require Import AST.
Require Import RTL.
-(* This is a port of tunneling for LTL. See Tunneling.v *)
+(* This is a port of tunneling for LTL. See LTLTunneling.v *)
Definition UF := PTree.t (node * Z).