From 8a8afc11df5dfe4755b7dd4344b6a27d198bd2e1 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 13 Nov 2017 15:36:38 -0500
Subject: Update GeneralizeVar to ensure Wf

This will hopefully pave the way for not needing to prove Wf anywhere in
the bounds pipeline.
---
 _CoqProject | 3 +++
 1 file changed, 3 insertions(+)

(limited to '_CoqProject')

diff --git a/_CoqProject b/_CoqProject
index e8d3b792d..0752ce47e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -161,6 +161,9 @@ src/Compilers/Z/CommonSubexpressionElimination.v
 src/Compilers/Z/CommonSubexpressionEliminationInterp.v
 src/Compilers/Z/CommonSubexpressionEliminationWf.v
 src/Compilers/Z/FoldTypes.v
+src/Compilers/Z/GeneralizeVar.v
+src/Compilers/Z/GeneralizeVarInterp.v
+src/Compilers/Z/GeneralizeVarWf.v
 src/Compilers/Z/HexNotationConstants.v
 src/Compilers/Z/Inline.v
 src/Compilers/Z/InlineConstAndOp.v
-- 
cgit v1.2.3