aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-11-01 21:14:39 -0400
committerGravatar Jason Gross <jgross@mit.edu>2016-11-01 21:14:39 -0400
commit0d4521cb7a7b75d49e2a83de611c464a71787b4e (patch)
treebcc7b9f5b95a180f18ea7b789212ae1929acfe71 /src
parent06e05ebb3e5225c3eb4c982a946aa13e9c6b5c35 (diff)
Export strings in GF25519Reflective/Common
This makes pretty-printing of bounds easier
Diffstat (limited to 'src')
-rw-r--r--src/Specific/GF25519Reflective/Common.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index b38ac0b44..8df44742e 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/Common.v
@@ -1,4 +1,5 @@
Require Export Coq.ZArith.ZArith.
+Require Export Coq.Strings.String.
Require Export Crypto.Specific.GF25519.
Require Import Crypto.Specific.GF25519BoundedCommon.
Require Import Crypto.Reflection.Reify.