File tree Expand file tree Collapse file tree 1 file changed +9
-1
lines changed
prusti-interface/src/environment Expand file tree Collapse file tree 1 file changed +9
-1
lines changed Original file line number Diff line number Diff line change @@ -523,10 +523,18 @@ impl<'tcx> Environment<'tcx> {
523523 called_def_id : ProcedureDefId , // what are we calling?
524524 call_substs : SubstsRef < ' tcx > ,
525525 ) -> ( ProcedureDefId , SubstsRef < ' tcx > ) {
526+ use prusti_rustc_interface:: middle:: ty:: TypeVisitable ;
527+
526528 // Avoids a compiler-internal panic
527529 // this check ignores any lifetimes/regions, which at this point would
528530 // need inference. They are thus ignored.
529- if self . any_type_needs_infer ( call_substs) {
531+ // TODO: different behaviour used for unsafe core proof
532+ let needs_infer = if config:: unsafe_core_proof ( ) {
533+ call_substs. needs_infer ( )
534+ } else {
535+ self . any_type_needs_infer ( call_substs)
536+ } ;
537+ if needs_infer {
530538 return ( called_def_id, call_substs) ;
531539 }
532540
You can’t perform that action at this time.
0 commit comments