git.iko.soy/Idris-dev
on master help sign in
Change forall tactic to use unify rather than isType

Fixes issue #189

commit35034db9661c30695243536d0d3bac4e71a4e861 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 18 Mar 2013, 23:37 (14 years ago) parentdb5973b
2 files changed+2−2
compare with master
unifiedsplit
CHANGELOG+1 src/Core/ProofState.hs+1−2
CHANGELOG+1
@@ -3,6 +3,7 @@ New in 0.9.8:
33
44User visible changes:
55
6+* Added "rewrite ... in ..." construct
67* Renamed EFF to EFFECT in Effect package
78* Experimental Java backend
89* Tab completion in REPL
src/Core/ProofState.hs+1−2
@@ -444,8 +444,7 @@ intro n ctxt env _ = fail "Can't introduce here."
444444forall :: Name -> Raw -> RunTactic
445445forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
446446 do (tyv, tyt) <- lift $ check ctxt env ty
447− lift $ isType ctxt env tyt
448− lift $ isType ctxt env t
447+ unify' ctxt env tyt (TType (UVar 0))
449448 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
450449forall n ty ctxt env _ = fail "Can't pi bind here"
451450