diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-02-15 14:31:58 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:39:04 -0400 |
| commit | 8873552ff45b5661b4e9dc7aefe42093588d0d6c (patch) | |
| tree | dcd37e69acf37e0431e83c727d168f8698f9ba20 | |
| parent | 9dcd8a07c2e11a4340449e20757dbf3ee8ba821e (diff) | |
changed the name of the ring to ring, not field
| -rw-r--r-- | src/ModularArithmetic/Tutorial.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v index c80decdcf..cabb8501b 100644 --- a/src/ModularArithmetic/Tutorial.v +++ b/src/ModularArithmetic/Tutorial.v @@ -15,7 +15,7 @@ Section Mod24. (* Boilerplate for [ring]. Similar boilerplate works for [field] if the modulus is prime . *) - Add Ring Ffield_q : (@Fring_theory q) + Add Ring Fring_q : (@Fring_theory q) (morphism (@Fring_morph q), preprocess [unfold ZToFq; Fpreprocess], postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], |