@@ -85,9 +85,9 @@ next (UN (x:xs)) = let (num', nm') = span isDigit (reverse x)
8585 readN "" = 0
8686 readN x = read x
8787
88−log :: String -> Elab ()
89−log str = do (p, logs) <- get
90− put (p, logs ++ str ++ "\n")
88+elog :: String -> Elab ()
89+elog str = do (p, logs) <- get
90+ put (p, logs ++ str ++ "\n")
9191
9292-- The primitives, from ProofState
9393
@@ -175,6 +175,13 @@ apply :: Raw -> [Bool] -> Elab ()
175175apply fn imps =
176176 do args <- prepare_apply fn imps
177177 fill (raw_apply fn (map Var args))
178+ -- *Don't* solve the arguments we're specifying by hand.
179+ -- (remove from unified list before calling end_unify)
180+ let dontunify = map fst (filter (not.snd) (zip args imps))
181+ (p, s) <- get
182+ let (n, hs) = unified p
183+ let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)
184+ put (p { unified = unify }, s)
178185 end_unify
179186
180187-- Abstract over an argument of unknown type, giving a name for the hole