Skip to content

Commit

Permalink
Tactic parser (tamarin-prover#531)
Browse files Browse the repository at this point in the history
* Correcting a typo

---------

Co-authored-by: Maiwenn Racouchot <mracouch@maiwenn.loria.fr>
Co-authored-by: Jannik Dreier <jannik.dreier@loria.fr>
Co-authored-by: jdreier <jdreier@users.noreply.github.com>
  • Loading branch information
4 people committed Apr 4, 2023
1 parent d9eaa24 commit 1bc24b9
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion lib/theory/src/Theory/Constraint/Solver/ProofMethod.hs
Original file line number Diff line number Diff line change
Expand Up @@ -640,7 +640,7 @@ itRanking tactic ags ctxt _sys = result
preorderedDeprio = if (Nothing `elem` indexDeprio) then map (snd . unzip) (tail groupedDeprio) else map (snd . unzip) groupedDeprio -- recovering ranked goals only (no prio = Nothing = fst)

deprioRankingFunctions = map rankingDeprio (_deprios tactic)
rankingFunToBeAppliedDeprio = chooseRankingFunctionByPrio deprioRankingFunctions (map head groupedPrio)
rankingFunToBeAppliedDeprio = chooseRankingFunctionByPrio deprioRankingFunctions (map head groupedDeprio)
deprioReorderedGoals = applyRankingFunctions rankingFunToBeAppliedDeprio preorderedDeprio

rankedDeprioGoals = concat deprioReorderedGoals
Expand Down

0 comments on commit 1bc24b9

Please sign in to comment.