diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-01 16:14:33 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 15:31:28 -0700 |
| commit | e43e4322481d1d90b74896de5cea886b1f87cca7 (patch) | |
| tree | a681d9e656a48e131332d23453acb1f896410c13 /_CoqProject | |
| parent | aa98370ba6165fb1f96b89645044ef13880bcf74 (diff) | |
PHOAS syntax
We also have linearization of function application / lets,
constant-inlining, and reification.
This closes #58.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 897d82a6c..ae4bea90f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -63,6 +63,13 @@ src/ModularArithmetic/BarrettReduction/ZHandbook.v src/ModularArithmetic/Montgomery/Z.v src/ModularArithmetic/Montgomery/ZBounded.v src/ModularArithmetic/Montgomery/ZProofs.v +src/Reflection/InputSyntax.v +src/Reflection/InterpProofs.v +src/Reflection/Linearize.v +src/Reflection/ReifyDirect.v +src/Reflection/ReifyExact.v +src/Reflection/Syntax.v +src/Reflection/TestCase.v src/Spec/CompleteEdwardsCurve.v src/Spec/EdDSA.v src/Spec/Encoding.v |