aboutsummaryrefslogtreecommitdiffstats
path: root/backend/LTLTunnelingaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'backend/LTLTunnelingaux.ml')
-rw-r--r--backend/LTLTunnelingaux.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/LTLTunnelingaux.ml b/backend/LTLTunnelingaux.ml
index c3b8cf82..66540bc1 100644
--- a/backend/LTLTunnelingaux.ml
+++ b/backend/LTLTunnelingaux.ml
@@ -3,6 +3,7 @@
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
+(* Pierre Goutagny ENS-Lyon, VERIMAG *)
(* *)
(* Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)