From 8b2f4db097dc91133cec138db2c70ebe11a35f22 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 15 Apr 2017 01:22:06 -0400
Subject: Add CSE correctness files for Z-specialization

They depend on admitted proofs, currently
---
 _CoqProject | 2 ++
 1 file changed, 2 insertions(+)

(limited to '_CoqProject')

diff --git a/_CoqProject b/_CoqProject
index 36cddc8ab..b41e8f6b9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -111,6 +111,8 @@ src/Compilers/Z/ArithmeticSimplifierWf.v
 src/Compilers/Z/BinaryNotationConstants.v
 src/Compilers/Z/CNotations.v
 src/Compilers/Z/CommonSubexpressionElimination.v
+src/Compilers/Z/CommonSubexpressionEliminationInterp.v
+src/Compilers/Z/CommonSubexpressionEliminationWf.v
 src/Compilers/Z/FoldTypes.v
 src/Compilers/Z/HexNotationConstants.v
 src/Compilers/Z/Inline.v
-- 
cgit v1.2.3