diff options
Diffstat (limited to 'src/Algebra')
| -rw-r--r-- | src/Algebra/IntegralDomain.v | 2 | ||||
| -rw-r--r-- | src/Algebra/Nsatz.v | 2 |
2 files changed, 2 insertions, 2 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. diff --git a/src/Algebra/Nsatz.v b/src/Algebra/Nsatz.v index 2a65e7d82..f1e031d32 100644 --- a/src/Algebra/Nsatz.v +++ b/src/Algebra/Nsatz.v @@ -108,7 +108,7 @@ Ltac nsatz_domain_sugar_power domain sugar power := intros _ (* discard [nsatz_compute] output *); intros; apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond)); [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS] - | solve [vm_compute; exact (eq_refl true)] (* exact_no_check (eq_refl true) *) + | solve [vm_cast_no_check (eq_refl true)] (* if this fails, the prover returned a bad certificate *) | solve [repeat (split; [assumption|]); exact I] ] end. |