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 ++++++
 backend/CSE2proof.v | 8 ++++++++
 2 files changed, 14 insertions(+)

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.
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index fe2ade4b..73feccf0 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -1,3 +1,11 @@
+(*
+Replace available expressions by the register containing their value.
+
+Proofs.
+
+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