aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-10-20 19:54:58 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-10-20 19:54:58 -0400
commita1c697281a1abce26b269eb4d5573e8356d653a0 (patch)
tree980122e95de3de40e1f0481f163e21961fd6a6c3 /_CoqProject
parent5830bc54939cf5dc8d10c02a7deeecf6df9067ca (diff)
Add Z.InlineConstAndOp*
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject3
1 files changed, 3 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index babe95a3a..e86e74678 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -149,6 +149,9 @@ src/Compilers/Z/CommonSubexpressionEliminationWf.v
src/Compilers/Z/FoldTypes.v
src/Compilers/Z/HexNotationConstants.v
src/Compilers/Z/Inline.v
+src/Compilers/Z/InlineConstAndOp.v
+src/Compilers/Z/InlineConstAndOpInterp.v
+src/Compilers/Z/InlineConstAndOpWf.v
src/Compilers/Z/InlineInterp.v
src/Compilers/Z/InlineWf.v
src/Compilers/Z/InterpSideConditions.v