1 files changed, 3 insertions, 3 deletions
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index 76efe3d79..8ee07fe5d 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -26,8 +26,8 @@ Section FieldOperations.
   Context {m : BinInt.Z}.
 
   (* Coercion without Context {m} --> non-uniform inheritance --> Anomalies *)
-  Local Coercion ZToFm := ZToField : BinNums.Z -> F m.
-  
+  Let ZToFm := ZToField : BinNums.Z -> F m. Local Coercion ZToFm : BinNums.Z >-> F.
+
   Definition add (a b:F m) : F m := ZToField (a + b).
   Definition mul (a b:F m) : F m := ZToField (a * b).
 
@@ -69,4 +69,4 @@ Infix "-" := sub : F_scope.
 Infix "/" := div : F_scope.
 Infix "^" := pow : F_scope.
 Notation "0" := (ZToField 0) : F_scope.
-Notation "1" := (ZToField 1) : F_scope.
-\ No newline at end of file
+Notation "1" := (ZToField 1) : F_scope.