[ #5388 ] Removed getInstantiatedMetas.

agda · Jan 12, 2022 · 860adc5 · 860adc5
1 parent 078362f
commit 860adc5
Showing 1 changed file with 0 additions and 9 deletions.
diff --git a/src/full/Agda/TypeChecking/Monad/MetaVars.hs b/src/full/Agda/TypeChecking/Monad/MetaVars.hs
@@ -552,15 +552,6 @@ getMetaVariables p = do
   store <- getMetaStore
   return [ MetaId i | (i, mv) <- IntMap.assocs store, p mv ]
 
-getInstantiatedMetas :: ReadTCState m => m [MetaId]
-getInstantiatedMetas = getMetaVariables (isInst . mvInstantiation)
-  where
-    isInst Open                           = False
-    isInst OpenInstance                   = False
-    isInst BlockedConst{}                 = False
-    isInst PostponedTypeCheckingProblem{} = False
-    isInst InstV{}                        = True
-
 getOpenMetas :: ReadTCState m => m [MetaId]
 getOpenMetas = getMetaVariables (isOpenMeta . mvInstantiation)