diff options
Diffstat (limited to 'src/Algebra/IntegralDomain.v')
| -rw-r--r-- | src/Algebra/IntegralDomain.v | 2 |
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. |