From 1dd98d18c57abdbc8dc50bbef729e8a898d55aad Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 3 Feb 2020 17:11:35 +0100
Subject: comments

---
 backend/CSE2.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'backend/CSE2.v')

diff --git a/backend/CSE2.v b/backend/CSE2.v
index f1ed877a..b7665097 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -1,3 +1,9 @@
+(*
+Replace available expressions by the register containing their value.
+
+David Monniaux, CNRS, VERIMAG
+ *)
+
 Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
 Require Import AST Linking.
 Require Import Memory Registers Op RTL Maps.
-- 
cgit