diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2015-10-22 13:07:57 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2015-10-22 13:07:57 -0400 |
| commit | cf9d1330a883d6ecf5afd43e96b086f4f99bf7e1 (patch) | |
| tree | ebf7b0d0fe74ea8b76b857370fbf4bbec8501071 /src/Galois/Galois.v | |
| parent | aa481c0d996c37220fac7d6ab0facb3f7cafe958 (diff) | |
fix the makefile to not rebuild + module renaming
Diffstat (limited to 'src/Galois/Galois.v')
| -rw-r--r-- | src/Galois/Galois.v | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/src/Galois/Galois.v b/src/Galois/Galois.v index 439b4735c..3ee86e4e4 100644 --- a/src/Galois/Galois.v +++ b/src/Galois/Galois.v @@ -4,10 +4,7 @@ Require Import Eqdep_dec. Require Import Tactics.VerdiTactics. Section GaloisPreliminaries. - Definition SMALL_THRESH: Z := 128. - Definition MIN_PRIME: Z := SMALL_THRESH * SMALL_THRESH. - - Definition Prime := {x: Z | prime x /\ x > MIN_PRIME}. + Definition Prime := {x: Z | prime x}. Definition primeToZ(x: Prime) := proj1_sig x. Coercion primeToZ: Prime >-> Z. @@ -51,9 +48,9 @@ Module Galois (M: Modulus). Definition GFone: GF. exists 1. - abstract (symmetry; apply Zmod_small; intuition; - destruct modulus; simpl; destruct a; - apply prime_ge_2 in H; intuition). + abstract( symmetry; apply Zmod_small; intuition; + destruct modulus; simpl; + apply prime_ge_2 in p; intuition). Defined. Definition GFplus(x y: GF): GF. |