aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ModularArithmeticTheorems.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-06-10 17:25:28 -0400
committerGravatar Jason Gross <jgross@mit.edu>2016-06-10 17:25:28 -0400
commit7129157393f420268c9399dc9b4119469994bf63 (patch)
tree62f4443c4e7b01c73e76af7589d20037386908d5 /src/ModularArithmetic/ModularArithmeticTheorems.v
parent969cb56234750c320768ae39e934b18ce2883aef (diff)
More changes for 8.5
[Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
Diffstat (limited to 'src/ModularArithmetic/ModularArithmeticTheorems.v')
-rw-r--r--src/ModularArithmetic/ModularArithmeticTheorems.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 8566177a1..6168f88bd 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -11,7 +11,7 @@ Require Export Crypto.Util.IterAssocOp.
Section ModularArithmeticPreliminaries.
Context {m:Z}.
- Local Coercion ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm.
+ Let ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.
Theorem F_eq: forall (x y : F m), x = y <-> FieldToZ x = FieldToZ y.
Proof.
@@ -318,7 +318,7 @@ End FandZ.
Section RingModuloPre.
Context {m:Z}.
- Local Coercion ZToFm' := ZToField : Z -> F m. Hint Unfold ZToFm'.
+ Let ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.
(* Substitution to prove all Compats *)
Ltac compat := repeat intro; subst; trivial.