No need to look for holes inside let bound values

...since we don't put holes there. This results in quite a gain in efficiency.

darcs-hash:20060802111332-974a0-003257f86c08488bc8018c790534ea4623d4cd05.gz

Ivor/Tactics.lhs

@@ -126,6 +126,7 @@ FIXME: Why not use a state monad for the unified variables in rt?
 >           rt env b@(Bind x (B (Let v) ty) _)
 >               | x == n = do (Ind b',u) <- tactic gam env (Ind b)
 >                             return (b',u)
+>               -- | otherwise = return (b, []) -- fail "No such hole"
 >           rt env b@(Bind x (B Lambda ty) _)
 >               | x == n = do (Ind b',u) <- tactic gam env (Ind b)
 >                             return (b',u)
@@ -148,8 +149,9 @@ FIXME: Why not use a state monad for the unified variables in rt?
 >                                          return (Stage (Escape t'), u)
 >           rt env x = return (x, [])
 >
->           rtb env (Let x) = do (rtx, u) <- rt env x
->                                return (Let rtx, u)
+>           -- No holes in let bound values!
+>           --rtb env (Let x) = do (rtx, u) <- rt env x
+>           --                     return (Let rtx, u)
 >           rtb env (Guess x) = do (rtx, u) <- rt env x
 >                                  return (Guess rtx, u)
 >           rtb env b = return (b, [])

ivor.cabal

@@ -6,7 +6,7 @@ License-file:	LICENSE
 Maintainer:	eb@dcs.st-and.ac.uk
 Homepage:	http://www.dcs.st-and.ac.uk/~eb/Ivor/
 Stability:	experimental
-Build-depends:	base, haskell98, util, parsec, mtl, Cabal
+Build-depends:	base, haskell98, util, parsec, mtl
 Extensions:	MultiParamTypeClasses, FunctionalDependencies,
 		ExistentialQuantification, OverlappingInstances
 ghc-prof-options: -auto-all