Skip to content

Commit 2ecba0f

Browse files
committed
Auto merge of #118937 - lcnr:rename-solver-flag, r=compiler-errors
`-Ztrait-solver=next` to `-Znext-solver` renames the feature flag to enable the new trait solver. still want some feedback before merging: https://rust-lang.zulipchat.com/#narrow/stream/364551-t-types.2Ftrait-system-refactor/topic/renaming.20the.20feature.20flag.20to.20.60-Znew-solver.60. The idea is to make it easier to add another option, e.g. to enable the solver in wfcheck or to optionally change its behavior to our new coinduction approach. r? `@compiler-errors`
2 parents 529047c + fa03289 commit 2ecba0f

File tree

274 files changed

+345
-333
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

274 files changed

+345
-333
lines changed

compiler/rustc_borrowck/src/region_infer/opaque_types.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -315,7 +315,7 @@ fn check_opaque_type_well_formed<'tcx>(
315315
parent_def_id = tcx.local_parent(parent_def_id);
316316
}
317317

318-
// FIXME(-Ztrait-solver=next): We probably should use `DefiningAnchor::Error`
318+
// FIXME(-Znext-solver): We probably should use `DefiningAnchor::Error`
319319
// and prepopulate this `InferCtxt` with known opaque values, rather than
320320
// using the `Bind` anchor here. For now it's fine.
321321
let infcx = tcx

compiler/rustc_borrowck/src/type_check/mod.rs

+3-3
Original file line numberDiff line numberDiff line change
@@ -1003,16 +1003,16 @@ impl<'a, 'tcx> TypeChecker<'a, 'tcx> {
10031003
reported_errors: Default::default(),
10041004
};
10051005

1006-
// FIXME(-Ztrait-solver=next): A bit dubious that we're only registering
1006+
// FIXME(-Znext-solver): A bit dubious that we're only registering
10071007
// predefined opaques in the typeck root.
10081008
if infcx.next_trait_solver() && !infcx.tcx.is_typeck_child(body.source.def_id()) {
1009-
checker.register_predefined_opaques_in_new_solver();
1009+
checker.register_predefined_opaques_for_next_solver();
10101010
}
10111011

10121012
checker
10131013
}
10141014

1015-
pub(super) fn register_predefined_opaques_in_new_solver(&mut self) {
1015+
pub(super) fn register_predefined_opaques_for_next_solver(&mut self) {
10161016
// OK to use the identity arguments for each opaque type key, since
10171017
// we remap opaques from HIR typeck back to their definition params.
10181018
let opaques: Vec<_> = self

compiler/rustc_codegen_cranelift/example/gen_block_iterate.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
// Copied from https://github.com/rust-lang/rust/blob/46455dc65069387f2dc46612f13fd45452ab301a/tests/ui/coroutine/gen_block_iterate.rs
22
// revisions: next old
33
//compile-flags: --edition 2024 -Zunstable-options
4-
//[next] compile-flags: -Ztrait-solver=next
4+
//[next] compile-flags: -Znext-solver
55
// run-pass
66
#![feature(gen_blocks)]
77

compiler/rustc_hir_analysis/src/check/compare_impl_item.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -320,7 +320,7 @@ fn compare_method_predicate_entailment<'tcx>(
320320
if check_implied_wf == CheckImpliedWfMode::Check && !(impl_sig, trait_sig).references_error() {
321321
// Select obligations to make progress on inference before processing
322322
// the wf obligation below.
323-
// FIXME(-Ztrait-solver=next): Not needed when the hack below is removed.
323+
// FIXME(-Znext-solver): Not needed when the hack below is removed.
324324
let errors = ocx.select_where_possible();
325325
if !errors.is_empty() {
326326
let reported = infcx.err_ctxt().report_fulfillment_errors(errors);
@@ -333,7 +333,7 @@ fn compare_method_predicate_entailment<'tcx>(
333333
// trigger the lint. Instead, let's only consider type outlives and
334334
// region outlives obligations.
335335
//
336-
// FIXME(-Ztrait-solver=next): Try removing this hack again once
336+
// FIXME(-Znext-solver): Try removing this hack again once
337337
// the new solver is stable.
338338
let mut wf_args: smallvec::SmallVec<[_; 4]> =
339339
unnormalized_impl_sig.inputs_and_output.iter().map(|ty| ty.into()).collect();

compiler/rustc_hir_typeck/src/coercion.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -1019,7 +1019,7 @@ impl<'a, 'tcx> FnCtxt<'a, 'tcx> {
10191019
/// Returns false if the coercion creates any obligations that result in
10201020
/// errors.
10211021
pub fn can_coerce(&self, expr_ty: Ty<'tcx>, target: Ty<'tcx>) -> bool {
1022-
// FIXME(-Ztrait-solver=next): We need to structurally resolve both types here.
1022+
// FIXME(-Znext-solver): We need to structurally resolve both types here.
10231023
let source = self.resolve_vars_with_obligations(expr_ty);
10241024
debug!("coercion::can_with_predicates({:?} -> {:?})", source, target);
10251025

compiler/rustc_hir_typeck/src/fn_ctxt/_impl.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ impl<'a, 'tcx> FnCtxt<'a, 'tcx> {
8383
/// version (resolve_vars_if_possible), this version will
8484
/// also select obligations if it seems useful, in an effort
8585
/// to get more type information.
86-
// FIXME(-Ztrait-solver=next): A lot of the calls to this method should
86+
// FIXME(-Znext-solver): A lot of the calls to this method should
8787
// probably be `try_structurally_resolve_type` or `structurally_resolve_type` instead.
8888
#[instrument(skip(self), level = "debug", ret)]
8989
pub(in super::super) fn resolve_vars_with_obligations(&self, mut ty: Ty<'tcx>) -> Ty<'tcx> {

compiler/rustc_infer/src/infer/canonical/mod.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,7 @@ impl<'tcx> InferCtxt<'tcx> {
101101
/// variable, then you'll get a new inference variable; if it is a
102102
/// universally quantified variable, you get a placeholder.
103103
///
104-
/// FIXME(-Ztrait-solver=next): This is public because it's used by the
104+
/// FIXME(-Znext-solver): This is public because it's used by the
105105
/// new trait solver which has a different canonicalization routine.
106106
/// We should somehow deduplicate all of this.
107107
pub fn instantiate_canonical_var(

compiler/rustc_infer/src/infer/canonical/substitute.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ use rustc_middle::ty::fold::{FnMutDelegate, TypeFoldable};
1111
use rustc_middle::ty::GenericArgKind;
1212
use rustc_middle::ty::{self, TyCtxt};
1313

14-
/// FIXME(-Ztrait-solver=next): This or public because it is shared with the
14+
/// FIXME(-Znext-solver): This or public because it is shared with the
1515
/// new trait solver implementation. We should deduplicate canonicalization.
1616
pub trait CanonicalExt<'tcx, V> {
1717
/// Instantiate the wrapped value, replacing each canonical value

compiler/rustc_infer/src/traits/mod.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -135,7 +135,7 @@ pub enum FulfillmentErrorCode<'tcx> {
135135
CodeSubtypeError(ExpectedFound<Ty<'tcx>>, TypeError<'tcx>), // always comes from a SubtypePredicate
136136
CodeConstEquateError(ExpectedFound<Const<'tcx>>, TypeError<'tcx>),
137137
CodeAmbiguity {
138-
/// Overflow reported from the new solver `-Ztrait-solver=next`, which will
138+
/// Overflow reported from the new solver `-Znext-solver`, which will
139139
/// be reported as an regular error as opposed to a fatal error.
140140
overflow: bool,
141141
},

compiler/rustc_interface/src/tests.rs

+7-5
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,9 @@ use rustc_session::config::{
66
build_configuration, build_session_options, rustc_optgroups, BranchProtection, CFGuard, Cfg,
77
DebugInfo, DumpMonoStatsFormat, ErrorOutputType, ExternEntry, ExternLocation, Externs,
88
FunctionReturn, InliningThreshold, Input, InstrumentCoverage, InstrumentXRay,
9-
LinkSelfContained, LinkerPluginLto, LocationDetail, LtoCli, MirSpanview, OomStrategy, Options,
10-
OutFileName, OutputType, OutputTypes, PAuthKey, PacRet, Passes, Polonius,
11-
ProcMacroExecutionStrategy, Strip, SwitchWithOptPath, SymbolManglingVersion, TraitSolver,
12-
WasiExecModel,
9+
LinkSelfContained, LinkerPluginLto, LocationDetail, LtoCli, MirSpanview, NextSolverConfig,
10+
OomStrategy, Options, OutFileName, OutputType, OutputTypes, PAuthKey, PacRet, Passes, Polonius,
11+
ProcMacroExecutionStrategy, Strip, SwitchWithOptPath, SymbolManglingVersion, WasiExecModel,
1312
};
1413
use rustc_session::lint::Level;
1514
use rustc_session::search_paths::SearchPath;
@@ -781,6 +780,10 @@ fn test_unstable_options_tracking_hash() {
781780
tracked!(mir_opt_level, Some(4));
782781
tracked!(move_size_limit, Some(4096));
783782
tracked!(mutable_noalias, false);
783+
tracked!(
784+
next_solver,
785+
Some(NextSolverConfig { coherence: true, globally: false, dump_tree: Default::default() })
786+
);
784787
tracked!(no_generate_arange_section, true);
785788
tracked!(no_jump_tables, true);
786789
tracked!(no_link, true);
@@ -822,7 +825,6 @@ fn test_unstable_options_tracking_hash() {
822825
tracked!(thir_unsafeck, true);
823826
tracked!(tiny_const_eval_limit, true);
824827
tracked!(tls_model, Some(TlsModel::GeneralDynamic));
825-
tracked!(trait_solver, TraitSolver::NextCoherence);
826828
tracked!(translate_remapped_path_to_local_path, false);
827829
tracked!(trap_unreachable, Some(false));
828830
tracked!(treat_err_as_bug, NonZeroUsize::new(1));

compiler/rustc_middle/src/traits/solve/cache.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ use rustc_data_structures::sync::Lock;
55
use rustc_query_system::cache::WithDepNode;
66
use rustc_query_system::dep_graph::DepNodeIndex;
77
use rustc_session::Limit;
8-
/// The trait solver cache used by `-Ztrait-solver=next`.
8+
/// The trait solver cache used by `-Znext-solver`.
99
///
1010
/// FIXME(@lcnr): link to some official documentation of how
1111
/// this works.

compiler/rustc_middle/src/ty/context.rs

+2-6
Original file line numberDiff line numberDiff line change
@@ -2240,15 +2240,11 @@ impl<'tcx> TyCtxt<'tcx> {
22402240
}
22412241

22422242
pub fn next_trait_solver_globally(self) -> bool {
2243-
self.sess.opts.unstable_opts.trait_solver == rustc_session::config::TraitSolver::Next
2243+
self.sess.opts.unstable_opts.next_solver.map_or(false, |c| c.globally)
22442244
}
22452245

22462246
pub fn next_trait_solver_in_coherence(self) -> bool {
2247-
matches!(
2248-
self.sess.opts.unstable_opts.trait_solver,
2249-
rustc_session::config::TraitSolver::Next
2250-
| rustc_session::config::TraitSolver::NextCoherence
2251-
)
2247+
self.sess.opts.unstable_opts.next_solver.map_or(false, |c| c.coherence)
22522248
}
22532249

22542250
pub fn is_impl_trait_in_trait(self, def_id: DefId) -> bool {

compiler/rustc_middle/src/ty/fast_reject.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ pub enum TreatParams {
6262
///
6363
/// N.B. during deep rejection, this acts identically to `ForLookup`.
6464
///
65-
/// FIXME(-Ztrait-solver=next): Remove this variant and cleanup
65+
/// FIXME(-Znext-solver): Remove this variant and cleanup
6666
/// the code.
6767
NextSolverLookup,
6868
}

compiler/rustc_session/src/config.rs

+13-12
Original file line numberDiff line numberDiff line change
@@ -755,13 +755,14 @@ pub enum PrintKind {
755755
}
756756

757757
#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
758-
pub enum TraitSolver {
759-
/// Classic trait solver in `rustc_trait_selection::traits::select`
760-
Classic,
761-
/// Experimental trait solver in `rustc_trait_selection::solve`
762-
Next,
763-
/// Use the new trait solver during coherence
764-
NextCoherence,
758+
pub struct NextSolverConfig {
759+
/// Whether the new trait solver should be enabled in coherence.
760+
pub coherence: bool,
761+
/// Whether the new trait solver should be enabled everywhere.
762+
/// This is only `true` if `coherence` is also enabled.
763+
pub globally: bool,
764+
/// Whether to dump proof trees after computing a proof tree.
765+
pub dump_tree: DumpSolverProofTree,
765766
}
766767

767768
#[derive(Default, Debug, Copy, Clone, Hash, PartialEq, Eq)]
@@ -3220,10 +3221,10 @@ pub(crate) mod dep_tracking {
32203221
use super::{
32213222
BranchProtection, CFGuard, CFProtection, CrateType, DebugInfo, DebugInfoCompression,
32223223
ErrorOutputType, FunctionReturn, InliningThreshold, InstrumentCoverage, InstrumentXRay,
3223-
LinkerPluginLto, LocationDetail, LtoCli, OomStrategy, OptLevel, OutFileName, OutputType,
3224-
OutputTypes, Polonius, RemapPathScopeComponents, ResolveDocLinks, SourceFileHashAlgorithm,
3225-
SplitDwarfKind, SwitchWithOptPath, SymbolManglingVersion, TraitSolver, TrimmedDefPaths,
3226-
WasiExecModel,
3224+
LinkerPluginLto, LocationDetail, LtoCli, NextSolverConfig, OomStrategy, OptLevel,
3225+
OutFileName, OutputType, OutputTypes, Polonius, RemapPathScopeComponents, ResolveDocLinks,
3226+
SourceFileHashAlgorithm, SplitDwarfKind, SwitchWithOptPath, SymbolManglingVersion,
3227+
TrimmedDefPaths, WasiExecModel,
32273228
};
32283229
use crate::lint;
32293230
use crate::utils::NativeLib;
@@ -3326,7 +3327,7 @@ pub(crate) mod dep_tracking {
33263327
BranchProtection,
33273328
OomStrategy,
33283329
LanguageIdentifier,
3329-
TraitSolver,
3330+
NextSolverConfig,
33303331
Polonius,
33313332
InliningThreshold,
33323333
FunctionReturn,

compiler/rustc_session/src/options.rs

+44-29
Original file line numberDiff line numberDiff line change
@@ -396,8 +396,7 @@ mod desc {
396396
pub const parse_instrument_xray: &str = "either a boolean (`yes`, `no`, `on`, `off`, etc), or a comma separated list of settings: `always` or `never` (mutually exclusive), `ignore-loops`, `instruction-threshold=N`, `skip-entry`, `skip-exit`";
397397
pub const parse_unpretty: &str = "`string` or `string=string`";
398398
pub const parse_treat_err_as_bug: &str = "either no value or a non-negative number";
399-
pub const parse_trait_solver: &str =
400-
"one of the supported solver modes (`classic`, `next`, or `next-coherence`)";
399+
pub const parse_next_solver_config: &str = "a comma separated list of solver configurations: `globally` (default), `coherence`, `dump-tree`, `dump-tree-on-error";
401400
pub const parse_lto: &str =
402401
"either a boolean (`yes`, `no`, `on`, `off`, etc), `thin`, `fat`, or omitted";
403402
pub const parse_linker_plugin_lto: &str =
@@ -429,7 +428,6 @@ mod desc {
429428
"a `,` separated combination of `bti`, `b-key`, `pac-ret`, or `leaf`";
430429
pub const parse_proc_macro_execution_strategy: &str =
431430
"one of supported execution strategies (`same-thread`, or `cross-thread`)";
432-
pub const parse_dump_solver_proof_tree: &str = "one of: `always`, `on-request`, `on-error`";
433431
pub const parse_remap_path_scope: &str = "comma separated list of scopes: `macro`, `diagnostics`, `unsplit-debuginfo`, `split-debuginfo`, `split-debuginfo-path`, `object`, `all`";
434432
pub const parse_inlining_threshold: &str =
435433
"either a boolean (`yes`, `no`, `on`, `off`, etc), or a non-negative number";
@@ -1032,15 +1030,48 @@ mod parse {
10321030
}
10331031
}
10341032

1035-
pub(crate) fn parse_trait_solver(slot: &mut TraitSolver, v: Option<&str>) -> bool {
1036-
match v {
1037-
Some("classic") => *slot = TraitSolver::Classic,
1038-
Some("next") => *slot = TraitSolver::Next,
1039-
Some("next-coherence") => *slot = TraitSolver::NextCoherence,
1040-
// default trait solver is subject to change..
1041-
Some("default") => *slot = TraitSolver::Classic,
1042-
_ => return false,
1033+
pub(crate) fn parse_next_solver_config(
1034+
slot: &mut Option<NextSolverConfig>,
1035+
v: Option<&str>,
1036+
) -> bool {
1037+
if let Some(config) = v {
1038+
let mut coherence = false;
1039+
let mut globally = true;
1040+
let mut dump_tree = None;
1041+
for c in config.split(',') {
1042+
match c {
1043+
"globally" => globally = true,
1044+
"coherence" => {
1045+
globally = false;
1046+
coherence = true;
1047+
}
1048+
"dump-tree" => {
1049+
if dump_tree.replace(DumpSolverProofTree::Always).is_some() {
1050+
return false;
1051+
}
1052+
}
1053+
"dump-tree-on-error" => {
1054+
if dump_tree.replace(DumpSolverProofTree::OnError).is_some() {
1055+
return false;
1056+
}
1057+
}
1058+
_ => return false,
1059+
}
1060+
}
1061+
1062+
*slot = Some(NextSolverConfig {
1063+
coherence: coherence || globally,
1064+
globally,
1065+
dump_tree: dump_tree.unwrap_or_default(),
1066+
});
1067+
} else {
1068+
*slot = Some(NextSolverConfig {
1069+
coherence: true,
1070+
globally: true,
1071+
dump_tree: Default::default(),
1072+
});
10431073
}
1074+
10441075
true
10451076
}
10461077

@@ -1305,19 +1336,6 @@ mod parse {
13051336
true
13061337
}
13071338

1308-
pub(crate) fn parse_dump_solver_proof_tree(
1309-
slot: &mut DumpSolverProofTree,
1310-
v: Option<&str>,
1311-
) -> bool {
1312-
match v {
1313-
None | Some("always") => *slot = DumpSolverProofTree::Always,
1314-
Some("never") => *slot = DumpSolverProofTree::Never,
1315-
Some("on-error") => *slot = DumpSolverProofTree::OnError,
1316-
_ => return false,
1317-
};
1318-
true
1319-
}
1320-
13211339
pub(crate) fn parse_inlining_threshold(slot: &mut InliningThreshold, v: Option<&str>) -> bool {
13221340
match v {
13231341
Some("always" | "yes") => {
@@ -1591,9 +1609,6 @@ options! {
15911609
"output statistics about monomorphization collection"),
15921610
dump_mono_stats_format: DumpMonoStatsFormat = (DumpMonoStatsFormat::Markdown, parse_dump_mono_stats, [UNTRACKED],
15931611
"the format to use for -Z dump-mono-stats (`markdown` (default) or `json`)"),
1594-
dump_solver_proof_tree: DumpSolverProofTree = (DumpSolverProofTree::Never, parse_dump_solver_proof_tree, [UNTRACKED],
1595-
"dump a proof tree for every goal evaluated by the new trait solver. If the flag is specified without any options after it
1596-
then it defaults to `always`. If the flag is not specified at all it defaults to `on-request`."),
15971612
dwarf_version: Option<u32> = (None, parse_opt_number, [TRACKED],
15981613
"version of DWARF debug information to emit (default: 2 or 4, depending on platform)"),
15991614
dylib_lto: bool = (false, parse_bool, [UNTRACKED],
@@ -1722,6 +1737,8 @@ options! {
17221737
"the size at which the `large_assignments` lint starts to be emitted"),
17231738
mutable_noalias: bool = (true, parse_bool, [TRACKED],
17241739
"emit noalias metadata for mutable references (default: yes)"),
1740+
next_solver: Option<NextSolverConfig> = (None, parse_next_solver_config, [TRACKED],
1741+
"enable and configure the next generation trait solver used by rustc"),
17251742
nll_facts: bool = (false, parse_bool, [UNTRACKED],
17261743
"dump facts from NLL analysis into side files (default: no)"),
17271744
nll_facts_dir: String = ("nll-facts".to_string(), parse_string, [UNTRACKED],
@@ -1922,8 +1939,6 @@ written to standard error output)"),
19221939
"for every macro invocation, print its name and arguments (default: no)"),
19231940
track_diagnostics: bool = (false, parse_bool, [UNTRACKED],
19241941
"tracks where in rustc a diagnostic was emitted"),
1925-
trait_solver: TraitSolver = (TraitSolver::Classic, parse_trait_solver, [TRACKED],
1926-
"specify the trait solver mode used by rustc (default: classic)"),
19271942
// Diagnostics are considered side-effects of a query (see `QuerySideEffects`) and are saved
19281943
// alongside query results and changes to translation options can affect diagnostics - so
19291944
// translation options should be tracked.

compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs

+6-5
Original file line numberDiff line numberDiff line change
@@ -200,9 +200,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
200200
let result = f(&mut ecx);
201201

202202
let tree = ecx.inspect.finalize();
203-
if let (Some(tree), DumpSolverProofTree::Always) =
204-
(&tree, infcx.tcx.sess.opts.unstable_opts.dump_solver_proof_tree)
205-
{
203+
if let (Some(tree), DumpSolverProofTree::Always) = (
204+
&tree,
205+
infcx.tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default(),
206+
) {
206207
let mut lock = std::io::stdout().lock();
207208
let _ = lock.write_fmt(format_args!("{tree:?}\n"));
208209
let _ = lock.flush();
@@ -377,7 +378,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
377378
//
378379
// This assert was removed as it did not hold for goals constraining
379380
// an inference variable to a recursive alias, e.g. in
380-
// tests/ui/traits/new-solver/overflow/recursive-self-normalization.rs.
381+
// tests/ui/traits/next-solver/overflow/recursive-self-normalization.rs.
381382
//
382383
// Once we have decided on how to handle trait-system-refactor-initiative#75,
383384
// we should re-add an assert here.
@@ -421,7 +422,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
421422
self.compute_const_evaluatable_goal(Goal { param_env, predicate: ct })
422423
}
423424
ty::PredicateKind::ConstEquate(_, _) => {
424-
bug!("ConstEquate should not be emitted when `-Ztrait-solver=next` is active")
425+
bug!("ConstEquate should not be emitted when `-Znext-solver` is active")
425426
}
426427
ty::PredicateKind::NormalizesTo(predicate) => {
427428
self.compute_normalizes_to_goal(Goal { param_env, predicate })

compiler/rustc_trait_selection/src/solve/inspect/build.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -265,7 +265,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
265265
GenerateProofTree::Never => ProofTreeBuilder::new_noop(),
266266
GenerateProofTree::IfEnabled => {
267267
let opts = &tcx.sess.opts.unstable_opts;
268-
match opts.dump_solver_proof_tree {
268+
match opts.next_solver.map(|c| c.dump_tree).unwrap_or_default() {
269269
DumpSolverProofTree::Always => ProofTreeBuilder::new_root(),
270270
// `OnError` is handled by reevaluating goals in error
271271
// reporting with `GenerateProofTree::Yes`.

0 commit comments

Comments
 (0)