aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-03-30 16:48:08 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-03-30 16:48:08 -0400
commitcb9e18103c6fe0580fa6598380b6c6ec66d261a0 (patch)
tree38a66c5c1f8d9f8d022fb44d5edb62148f5b29bb /_CoqProject
parent7d70da13d3d44c6eed92dfd490138d7a05120208 (diff)
Don't linearize and eta in MapCastByDeBruijn
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject2
1 files changed, 1 insertions, 1 deletions
diff --git a/_CoqProject b/_CoqProject
index 23236fd4a..0cec928e7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -187,7 +187,6 @@ src/Reflection/Named/ContextProperties/Tactics.v
src/Reflection/Named/PositiveContext/Defaults.v
src/Reflection/Named/PositiveContext/DefaultsProperties.v
src/Reflection/Z/BinaryNotationConstants.v
-src/Reflection/Z/BoundsInterpretations.v
src/Reflection/Z/CNotations.v
src/Reflection/Z/FoldTypes.v
src/Reflection/Z/HexNotationConstants.v
@@ -198,6 +197,7 @@ src/Reflection/Z/JavaNotations.v
src/Reflection/Z/OpInversion.v
src/Reflection/Z/Reify.v
src/Reflection/Z/Syntax.v
+src/Reflection/Z/Bounds/Interpretation.v
src/Reflection/Z/Interpretations128/Relations.v
src/Reflection/Z/Interpretations128/RelationsCombinations.v
src/Reflection/Z/Interpretations64/Relations.v