aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-09-05 20:04:08 -0700
committerGravatar Jason Gross <jagro@google.com>2016-09-05 20:04:08 -0700
commit235e58e2233a5c13a2065fdcd85073e016cad3df (patch)
tree0fd13b45af3e8debc69478f0abaf22fab1aa8357 /_CoqProject
parent0cb8d2bd781c8094e32ff1de78e461bd44d3ea7e (diff)
Add LinearizeWf
The proof of wf-preservation for inline_const isn't finished yet, though...
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject1
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index e451e264c..8dac65e12 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -66,6 +66,7 @@ src/ModularArithmetic/Montgomery/ZProofs.v
src/Reflection/InputSyntax.v
src/Reflection/InterpProofs.v
src/Reflection/Linearize.v
+src/Reflection/LinearizeWf.v
src/Reflection/Reify.v
src/Reflection/Syntax.v
src/Reflection/TestCase.v