@@ -881,15 +881,11 @@ elab ist info emode opts fn tm
881881 -- names which have been used elsewhere in the term, since we
882882 -- won't be able to use them in the resulting application.
883883 let unique_used = getUniqueUsed (tt_ctxt ist) ptm
884− let n' = mkN n
884+ let n' = metavarName (namespace info) n
885885 attack
886886 defer unique_used n'
887887 solve
888888 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)
889− where mkN n@(NS _ _) = n
890− mkN n = case namespace info of
891− Just xs@(_:_) -> sNS n xs
892− _ -> n
893889 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts
894890 elab' ina fc (PTactics ts)
895891 | not pattern = do mapM_ (runTac False ist fc fn) ts
@@ -1696,6 +1692,11 @@ case_ ind autoSolve ist fn tm = do
16961692 else casetac (forget val)
16971693 when autoSolve solveAll
16981694
1695+-- | Compute the appropriate name for a top-level metavariable
1696+metavarName :: Maybe [String] -> Name -> Name
1697+metavarName _ n@(NS _ _) = n
1698+metavarName (Just (ns@(_:_))) n = sNS n ns
1699+metavarName _ n = n
16991700
17001701runTactical :: IState -> FC -> Env -> Term -> [String] -> ElabD Term
17011702runTactical ist fc env tm ns = do tm' <- eval tm
@@ -1974,6 +1975,17 @@ runTactical ist fc env tm ns = do tm' <- eval tm
19741975 fmap fst . checkClosed $
19751976 rawPair (Var $ reflm "TT", Var $ reflm "TT")
19761977 (tm', ty')
1978+ | n == tacN "prim__Metavar", [n] <- args
1979+ = do n' <- reifyTTName n
1980+ ctxt <- get_context
1981+ ptm <- get_term
1982+ -- See documentation above in the elab case for PMetavar
1983+ let unique_used = getUniqueUsed ctxt ptm
1984+ let mvn = metavarName (Just ns) n'
1985+ attack
1986+ defer unique_used mvn
1987+ solve
1988+ returnUnit
19771989 | n == tacN "prim__Debug", [ty, msg] <- args
19781990 = do msg' <- eval msg
19791991 parts <- reifyReportParts msg