[ Rewriting ] Better blocking tags

agda · Oct 16, 2015 · cc13509 · cc13509
1 parent 8aaf105
commit cc13509
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
@@ -245,9 +245,11 @@ instance Match NLPat Term where
         match k p' body
       PPi pa pb  -> case ignoreSharing v of
         Pi a b -> match k pa a >> match k pb b
+        MetaV m es -> matchingBlocked $ Blocked m ()
         _ -> no
       PBoundVar i ps -> case ignoreSharing v of
         Var i' es | i == i' -> matchArgs k ps es
+        MetaV m es -> matchingBlocked $ Blocked m ()
         _ -> no
       PTerm u -> tellEq k u v
     where