Skip to content

Commit

Permalink
revert lifting of uvar ctx in withUVars
Browse files Browse the repository at this point in the history
  • Loading branch information
m-yac committed Aug 16, 2022
1 parent c18c121 commit 59dfb09
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/SAWScript/Prover/MRSolver/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -679,7 +679,7 @@ withUVars :: [(LocalName,Term)] -> ([Term] -> MRM a) -> MRM a
withUVars [] f = f []
withUVars ctx f =
do nms <- uniquifyNames (map fst ctx) <$> map fst <$> mrUVars
ctx_u <- zip nms <$> mapM (liftTermLike 0 (length ctx) . Type . snd) ctx
let ctx_u = zip nms $ map (Type . snd) ctx
assumps' <- mrAssumptions >>= liftTerm 0 (length ctx)
dataTypeAssumps' <- mrDataTypeAssumps >>= mapM (liftTermLike 0 (length ctx))
vars <- reverse <$> mapM (liftSC1 scLocalVar) [0 .. length ctx - 1]
Expand Down

0 comments on commit 59dfb09

Please sign in to comment.