diff options
Diffstat (limited to 'src/Algebra/Nsatz.v')
| -rw-r--r-- | src/Algebra/Nsatz.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |