diff options
Diffstat (limited to 'source/Checking/Declaration.hs')
| -rw-r--r-- | source/Checking/Declaration.hs | 19 |
1 files changed, 6 insertions, 13 deletions
diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs index 65b7675..f95286c 100644 --- a/source/Checking/Declaration.hs +++ b/source/Checking/Declaration.hs @@ -2817,20 +2817,14 @@ prepareVampireObligationWith globalType builder selection - let (globalMode, localPolicy) = + let premiseSelection = case selection of VampireImplicitPremises -> - ( Backend.ImplicitFofPremises - , Backend.FirstOrderLocals - ) + Backend.ImplicitPremiseSelection VampireExplicitPremises{} -> - ( Backend.ExplicitGlobalPremises - , Backend.FirstOrderLocals - ) + Backend.ExplicitGlobalPremiseSelection VampireLocalPremises -> - ( Backend.NoGlobalPremises - , Backend.AllLocals - ) + Backend.LocalOnlyPremiseSelection propositionDependencies = foundationAxiomDependencies . Backend.supportedPropositionTerm @@ -2846,7 +2840,7 @@ prepareVampireObligationWith (propositionDependencies . Backend.typedLocalPremiseProposition) (Backend.selectTypedLocalPremises - localPolicy + premiseSelection locals) ) auxiliaries = @@ -2861,8 +2855,7 @@ prepareVampireObligationWith claim locals auxiliaries - globalMode - localPolicy) + premiseSelection) task <- first VampireObligationEncodingFailed (Provers.prepareTypedProverTask |