aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-04-02 00:57:57 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-04-02 00:57:57 -0400
commitc04db8623eaf1fccebd663975eb25e58ea346b86 (patch)
tree7f0c567c711cac88614dd0e858fc418e6ba56bec /_CoqProject
parent9aa5f21e5239c031cfa3b3dc3df8166e9153435d (diff)
Add Z instantiations of InlineConst
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject3
1 files changed, 3 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index 8375be807..30f5a6b33 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -200,6 +200,9 @@ src/Reflection/Z/BinaryNotationConstants.v
src/Reflection/Z/CNotations.v
src/Reflection/Z/FoldTypes.v
src/Reflection/Z/HexNotationConstants.v
+src/Reflection/Z/Inline.v
+src/Reflection/Z/InlineInterp.v
+src/Reflection/Z/InlineWf.v
src/Reflection/Z/Interpretations128.v
src/Reflection/Z/Interpretations64.v
src/Reflection/Z/InterpretationsGen.v