Permalink
Browse files

Induction normalises the target first

Ignore-this: 63cf0f91daa0a1e85f1ac8bb44e78ba5

darcs-hash:20090727011757-228f4-c84267185e0ab255630585930bf85534c43d5202.gz
  • Loading branch information...
1 parent d5156cf commit a5a8f8f04df08f622bcb2b1c664115d6d10e9d30 eb committed Jul 27, 2009
Showing with 7 additions and 4 deletions.
  1. +3 −2 Ivor/Tactics.lhs
  2. +1 −1 ivor.cabal
  3. +3 −1 release/Release.lhs
View
@@ -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
View
@@ -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,
View
@@ -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

0 comments on commit a5a8f8f

Please sign in to comment.