aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra/IntegralDomain.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Algebra/IntegralDomain.v')
-rw-r--r--src/Algebra/IntegralDomain.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
index c52b4ce87..5733d5cca 100644
--- a/src/Algebra/IntegralDomain.v
+++ b/src/Algebra/IntegralDomain.v
@@ -165,7 +165,7 @@ Module IntegralDomain.
let x' := constr:(@_LargeCharacteristicReflective.denote R one opp add mul x') in
change (not (eq x' zero));
apply (_LargeCharacteristicReflective.is_nonzero_correct(eq:=eq)(zero:=zero) C cg);
- abstract (vm_cast_no_check (eq_refl true))
+ (vm_cast_no_check (eq_refl true))
end
end.
End IntegralDomain.