aboutsummaryrefslogtreecommitdiffstats
path: root/backend/LTLTunnelingaux.ml
diff options
context:
space:
mode:
authorSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2021-08-24 11:35:58 +0200
committerSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2021-08-24 11:35:58 +0200
commit74901c6df6ceb92da58ef5db2592fc05561dce01 (patch)
tree0ce0f3ac7d3ccad31927fe8777773c4eba0d1051 /backend/LTLTunnelingaux.ml
parent4f23d3753fd51233e337fcf76c2f1abfafb2b280 (diff)
downloadcompcert-kvx-74901c6df6ceb92da58ef5db2592fc05561dce01.tar.gz
compcert-kvx-74901c6df6ceb92da58ef5db2592fc05561dce01.zip
RTLTunneling: fix comments and authors information
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 *)