@@ -162,9 +162,9 @@ elab ist info pattern opts fn tm
163 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
163 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
164 elab' ina PType = do apply RType []; solve
164 elab' ina PType = do apply RType []; solve
165− elab' (_,_,inty) (PConstant c)
165+-- elab' (_,_,inty) (PConstant c)
166− | constType c && pattern && not reflect && not inty
166+-- | constType c && pattern && not reflect && not inty
167− = lift $ tfail (Msg "Typecase is not allowed")
167+-- = lift $ tfail (Msg "Typecase is not allowed")
168 elab' ina (PConstant c) = do apply (RConstant c) []; solve
168 elab' ina (PConstant c) = do apply (RConstant c) []; solve
169 elab' ina (PQuote r) = do fill r; solve
169 elab' ina (PQuote r) = do fill r; solve
170 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
170 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
@@ -240,9 +240,9 @@ elab ist info pattern opts fn tm
240 trySeq' deferr (x : xs)
240 trySeq' deferr (x : xs)
241 = try' (elab' ina x) (trySeq' deferr xs) True
241 = try' (elab' ina x) (trySeq' deferr xs) True
242 elab' ina (PPatvar fc n) | pattern = patvar n
242 elab' ina (PPatvar fc n) | pattern = patvar n
243− elab' (_, _, inty) (PRef fc f)
243+-- elab' (_, _, inty) (PRef fc f)
244− | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
244+-- | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
245− = lift $ tfail (Msg "Typecase is not allowed")
245+-- = lift $ tfail (Msg "Typecase is not allowed")
246 elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
246 elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
247 = do ctxt <- get_context
247 = do ctxt <- get_context
248 let defined = case lookupTy n ctxt of
248 let defined = case lookupTy n ctxt of