Skip to content

Commit

Permalink
fixed withLocalLocalEnvironment to save the entire environment, not j…
Browse files Browse the repository at this point in the history
…ust parts of it
  • Loading branch information
Eddy Westbrook committed Dec 8, 2020
1 parent 5aa04fb commit 5a37203
Showing 1 changed file with 2 additions and 4 deletions.
6 changes: 2 additions & 4 deletions src/Verifier/SAW/Translation/Coq/Term.hs
Original file line number Diff line number Diff line change
Expand Up @@ -289,11 +289,9 @@ asApplyAllRecognizer t = do _ <- asApp t
-- restoring the current environment before returning.
withLocalLocalEnvironment :: TermTranslationMonad m => m a -> m a
withLocalLocalEnvironment action = do
env <- view localEnvironment <$> get
used <- view unavailableIdents <$> get
s <- get
result <- action
modify $ set localEnvironment env
modify $ set unavailableIdents used
put s
return result

mkDefinition :: Coq.Ident -> Coq.Term -> Coq.Decl
Expand Down

0 comments on commit 5a37203

Please sign in to comment.