Skip to content

Commit

Permalink
resolve warning, remove old comment
Browse files Browse the repository at this point in the history
  • Loading branch information
m-yac committed Mar 1, 2022
1 parent 7df316c commit 1f4ebc2
Showing 1 changed file with 1 addition and 3 deletions.
4 changes: 1 addition & 3 deletions src/SAWScript/Prover/MRSolver/Solver.hs
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,6 @@ import qualified Data.Map as Map
import Verifier.SAW.Term.Functor
import Verifier.SAW.SharedTerm
import Verifier.SAW.Recognizer
import Verifier.SAW.Term.Pretty

import SAWScript.Prover.MRSolver.Term
import SAWScript.Prover.MRSolver.Monad
Expand Down Expand Up @@ -613,8 +612,6 @@ withCoIndHyp f1 args1 f2 args2 m =
do ctx <- mrUVarCtx
withCoIndHyp' (CoIndHyp ctx f1 f2 args1 args2) m

-- | Test if a 'MRFailure' contains a widening

-- | The main loop of 'withCoIndHyp'
withCoIndHyp' :: CoIndHyp -> MRM a -> MRM a
withCoIndHyp' hyp m =
Expand All @@ -628,6 +625,7 @@ withCoIndHyp' hyp m =
withCoIndHyp' hyp' m
e -> throwError e


-- | Test that a coinductive hypothesis for the given function names matches the
-- given arguments, otherwise throw an exception saying that widening is needed
matchCoIndHyp :: CoIndHyp -> [Term] -> [Term] -> MRM ()
Expand Down

0 comments on commit 1f4ebc2

Please sign in to comment.