From 5a37203a2c5d0f78faf1faa3ebc8ab3cbeacae2d Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 7 Dec 2020 16:53:03 -0800 Subject: [PATCH] fixed withLocalLocalEnvironment to save the entire environment, not just parts of it --- src/Verifier/SAW/Translation/Coq/Term.hs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Verifier/SAW/Translation/Coq/Term.hs b/src/Verifier/SAW/Translation/Coq/Term.hs index 94bf6cff16..4e2e442d30 100644 --- a/src/Verifier/SAW/Translation/Coq/Term.hs +++ b/src/Verifier/SAW/Translation/Coq/Term.hs @@ -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