@@ -85,9 +85,9 @@ next (UN (x:xs)) = let (num', nm') = span isDigit (reverse x)
85 readN "" = 0
85 readN "" = 0
86 readN x = read x
86 readN x = read x
88−log :: String -> Elab ()
88+elog :: String -> Elab ()
89−log str = do (p, logs) <- get
89+elog str = do (p, logs) <- get
90− put (p, logs ++ str ++ "\n")
90+ put (p, logs ++ str ++ "\n")
92-- The primitives, from ProofState
92-- The primitives, from ProofState
@@ -175,6 +175,13 @@ apply :: Raw -> [Bool] -> Elab ()
175apply fn imps =
175apply fn imps =
176 do args <- prepare_apply fn imps
176 do args <- prepare_apply fn imps
177 fill (raw_apply fn (map Var args))
177 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))
182+ let (n, hs) = unified p
183+ let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)
184+ put (p { unified = unify }, s)
178 end_unify
185 end_unify
180-- Abstract over an argument of unknown type, giving a name for the hole
187-- Abstract over an argument of unknown type, giving a name for the hole