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