aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-09-15 16:14:11 -0700
committerGravatar Jason Gross <jagro@google.com>2016-09-15 16:14:11 -0700
commit2ab5de84a35cee04cc2768d88efcb684f1563507 (patch)
tree3b7d7f68f00cc7a4afa12ff9844937d4c3dff393 /_CoqProject
parent1ecf2f9945a99b5e4a58ebe46ec5764f07ec05aa (diff)
Add generalized version of Wf parameterized on rel
This should allow a nice elegant abstract way of doing bounds analysis. It's possible that wf should be redefined in terms of rel_wf.
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject1
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index 6cbebb799..6e6ce09d8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -74,6 +74,7 @@ src/Reflection/Syntax.v
src/Reflection/TestCase.v
src/Reflection/WfProofs.v
src/Reflection/WfReflective.v
+src/Reflection/WfRel.v
src/Spec/CompleteEdwardsCurve.v
src/Spec/EdDSA.v
src/Spec/Encoding.v