diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-13 15:36:38 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-13 15:37:16 -0500 |
| commit | 8a8afc11df5dfe4755b7dd4344b6a27d198bd2e1 (patch) | |
| tree | deb91aff06fd31917b81ad10c085322af0e32b0f /_CoqProject | |
| parent | b2a1a0c0360ae4cb35f0bcfb34bb86b4734c4800 (diff) | |
Update GeneralizeVar to ensure Wf
This will hopefully pave the way for not needing to prove Wf anywhere in
the bounds pipeline.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 3 |
1 files changed, 3 insertions, 0 deletions
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 |