diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-02-15 14:31:58 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-02-15 14:31:58 -0500 |
| commit | 89ed926fc9c5ca47b33b15dfd9f4558ae6738642 (patch) | |
| tree | f68504d8427292b1179ec790452df12d965d9c34 /src | |
| parent | c92678ddbbbc0c2bcfe8ee211cbdf1908e6beeab (diff) | |
changed the name of the ring to ring, not field
Diffstat (limited to 'src')
| -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], |