@@ -171,9 +171,9 @@ elab ist info pattern opts fn tm
171171 -> ElabD ()
172172 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
173173 elab' ina PType = do apply RType []; solve
174− elab' (_,_,inty) (PConstant c)
175− | constType c && pattern && not reflect && not inty
176− = lift $ tfail (Msg "Typecase is not allowed")
174+-- elab' (_,_,inty) (PConstant c)
175+-- | constType c && pattern && not reflect && not inty
176+-- = lift $ tfail (Msg "Typecase is not allowed")
177177 elab' ina (PConstant c) = do apply (RConstant c) []; solve
178178 elab' ina (PQuote r) = do fill r; solve
179179 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
@@ -245,9 +245,9 @@ elab ist info pattern opts fn tm
245245 trySeq' deferr (x : xs)
246246 = try' (elab' ina x) (trySeq' deferr xs) True
247247 elab' ina (PPatvar fc n) | pattern = patvar n
248− elab' (_, _, inty) (PRef fc f)
249− | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
250− = lift $ tfail (Msg "Typecase is not allowed")
248+-- elab' (_, _, inty) (PRef fc f)
249+-- | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
250+-- = lift $ tfail (Msg "Typecase is not allowed")
251251 elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
252252 = do ctxt <- get_context
253253 let defined = case lookupTy n ctxt of