diff --git a/src/TTImp/Interactive/GenerateDef.idr b/src/TTImp/Interactive/GenerateDef.idr index ab30db214..77eb6eef0 100644 --- a/src/TTImp/Interactive/GenerateDef.idr +++ b/src/TTImp/Interactive/GenerateDef.idr @@ -56,7 +56,7 @@ expandClause : {auto c : Ref Ctxt Defs} -> Core (Search (List ImpClause)) expandClause loc opts n c = do c <- uniqueRHS c - Right clause <- checkClause linear Private False n [] (MkNested []) [] c + Right clause <- checkClause linear Private PartialOK False n [] (MkNested []) [] c | Left err => noResult -- TODO: impossible clause, do something -- appropriate