aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar jadep <jade.philipoom@gmail.com>2019-04-03 12:14:52 -0400
committerGravatar jadephilipoom <jade.philipoom@gmail.com>2019-04-03 23:34:53 +0100
commitee30e8faf778ac9fd43f1d8d9d6d61cd4e9d8b3f (patch)
tree28a450c7645bcdc45c2ae32dc5d120509bc30419
parent18afe6845b715b69f6e4d13d884a9ff27434bde7 (diff)
fix typo
-rw-r--r--src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v b/src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
index 84d5be615..535e325dd 100644
--- a/src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
+++ b/src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
@@ -1,4 +1,4 @@
-(** * Push-Button Snthesis of fancy mongomery reduction : Reification Cache *)
+(** * Push-Button Synthesis of fancy mongomery reduction : Reification Cache *)
Require Import Coq.ZArith.ZArith.
Require Import Coq.derive.Derive.
Require Import Crypto.Arithmetic.Core.