Make "forget" actually forget in reflected Elab
commit3fe74aa6a777b59aebb301565a36891dd562201d
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateWed 15 Apr 2015, 13:16 (12 years ago)
parent6c7c887
src/Idris/ElabTerm.hs+1−1
@@ -1706,7 +1706,7 @@ runTactical fc env tm = do tm' <- eval tm
17061706 returnUnit
17071707 | n == tacN "prim__Forget", [tt] <- args
17081708 = do tt' <- reifyTT tt
1709− fmap fst . get_type_val $ reflect tt'
1709+ fmap fst . get_type_val . reflectRaw $ forget tt'
17101710 | n == tacN "prim__Attack", [] <- args
17111711 = do attack
17121712 returnUnit