Induction normalises the target first

Ignore-this: 63cf0f91daa0a1e85f1ac8bb44e78ba5

darcs-hash:20090727011757-228f4-c84267185e0ab255630585930bf85534c43d5202.gz

Ivor/Tactics.lhs

@@ -471,9 +471,10 @@ otherwise.
 
 > casetac :: Bool -> Raw -> Tactic
 > casetac rec scrutinee gam env tm@(Ind (Bind x (B Hole ty) sc)) =
->     do (Ind bv,bt) <- check gam (ptovenv env) scrutinee Nothing
+>     do (bv,bt) <- check gam (ptovenv env) scrutinee Nothing
 >        let (Ind btnorm) = (normaliseEnv (ptovenv env) gam bt)
->        let bvin = makePsEnv (map fst env) bv
+>        let (Ind bvnorm) = (normaliseEnv (ptovenv env) gam bv)
+>        let bvin = makePsEnv (map fst env) bvnorm
 >        let btin = makePsEnv (map fst env) btnorm
 >        let indices = getArgs btin
 >        let ty = getFun btin

ivor.cabal

@@ -58,7 +58,7 @@ Extra-source-files: emacs/ivor-mode.el, examplett/staged.tt, examplett/test.c, e
 
 
 
-Build-depends:  base, parsec, mtl, directory
+Build-depends:  base >=3 && <5, parsec, mtl, directory
 Build-type:     Simple
 
 Extensions:     MultiParamTypeClasses, FunctionalDependencies,

release/Release.lhs

@@ -8,8 +8,10 @@ and upload it.
 > import System.Environment
 > import System.Exit
 > import System.Directory
-> import System.Process
+> import System.Process hiding (shell)
 > import Distribution.PackageDescription
+> import Distribution.PackageDescription.Parse
+> import Distribution.PackageDescription.Configuration
 > import Distribution.Package
 > import Distribution.Verbosity
 > import Data.Version