From 4b018cdc72ecf3f940e6f352beb98a94ab567b33 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Oct 2022 19:51:56 -0700
Subject: [PATCH] chore: missing annotations

---
 src/Lean/Environment.lean    | 1 +
 src/Lean/MetavarContext.lean | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 8ea1b315ff..93690de4d3 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -869,6 +869,7 @@ class MonadEnv (m : Type → Type) where
 
 export MonadEnv (getEnv modifyEnv)
 
+@[alwaysInline]
 instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where
   getEnv    := liftM (getEnv : m Environment)
   modifyEnv := fun f => liftM (modifyEnv f : m Unit)
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 126475c775..b15fafae8d 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -330,6 +330,7 @@ class MonadMCtx (m : Type → Type) where
 
 export MonadMCtx (getMCtx modifyMCtx)
 
+@[alwaysInline]
 instance (m n) [MonadLift m n] [MonadMCtx m] : MonadMCtx n where
   getMCtx    := liftM (getMCtx : m _)
   modifyMCtx := fun f => liftM (modifyMCtx f : m _)