diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2015-12-12 23:43:35 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2015-12-12 23:43:35 -0500 |
| commit | 831496c8e896a32d6e7a969774acde8d4dd8fd18 (patch) | |
| tree | 0e4b947b36c0ee4f161eae6874592e65fe15ccaa /src/Galois/BaseSystem.v | |
| parent | 7e92e085e9eae37daff7553caeb9e6cff65cf569 (diff) | |
EdDSA: mostly-complete spec and preliminary structure.
Diffstat (limited to 'src/Galois/BaseSystem.v')
| -rw-r--r-- | src/Galois/BaseSystem.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 8197bed8d..28ae37233 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -39,7 +39,7 @@ Module BaseSystem (Import B:BaseCoefs). Lemma decode'_truncate : forall bs us, decode' bs us = decode' bs (firstn (length bs) us). Proof. - unfold decode, decode'; intros; f_equal; apply combine_truncate_l. + unfold decode'; intros; f_equal; apply combine_truncate_l. Qed. Fixpoint add (us vs:digits) : digits := |