aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Tunneling.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Tunneling.v')
-rw-r--r--backend/Tunneling.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index a4c4a195..78458582 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -101,5 +101,5 @@ Definition tunnel_function (f: LTL.function) : LTL.function :=
Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef :=
transf_fundef tunnel_function f.
-Definition tunnel_program (p: LTL.program) : LTL.program :=
+Definition transf_program (p: LTL.program) : LTL.program :=
transform_program tunnel_fundef p.