From f570d2a1c302499e2846595efefdb72eeed2417f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Dec 2019 16:14:26 -0800 Subject: [PATCH] fix: caching condition --- src/Init/Lean/Meta/SynthInstance.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean index 001bb72fba..3914c3209e 100644 --- a/src/Init/Lean/Meta/SynthInstance.lean +++ b/src/Init/Lean/Meta/SynthInstance.lean @@ -530,10 +530,10 @@ usingTransparency TransparencyMode.reducible $ do (pure (some result))) (pure none) }; - if type.hasMVar then do - modify $ fun s => { cache := { synthInstance := s.cache.synthInstance.insert type result, .. s.cache }, .. s }; + if type.hasMVar then pure result - else + else do + modify $ fun s => { cache := { synthInstance := s.cache.synthInstance.insert type result, .. s.cache }, .. s }; pure result /--