From 394047906dffd34ccc06f4525ec9633188f0ae2b Mon Sep 17 00:00:00 2001
From: Matus Tejiscak <ziman@functor.sk>
Date: Fri, 22 May 2020 20:29:56 +0200
Subject: [PATCH] Fix porting errors.

---
 src/Idris/Parser.idr    | 6 +++---
 src/TTImp/Elab/Term.idr | 3 +--
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index bd0df7408..5bd4f1d30 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -189,7 +189,7 @@ mutual
            symbol "}"
            pure (Nothing, tm)
 
-  with_ : FileName -> IndentInfo -> Rule PTerm
+  with_ : FileName -> IndentInfo -> SourceRule PTerm
   with_ fname indents
       = do start <- location
            keyword "with"
@@ -199,12 +199,12 @@ mutual
            rhs <- expr pdef fname indents
            pure (PWithUnambigNames (MkFC fname start end) ns rhs)
     where
-      singleName : Rule (List Name)
+      singleName : SourceRule (List Name)
       singleName = do
         n <- name
         pure [n]
 
-      nameList : Rule (List Name)
+      nameList : SourceRule (List Name)
       nameList = do
         symbol "["
         commit
diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr
index c6af330e6..cf08f00a6 100644
--- a/src/TTImp/Elab/Term.idr
+++ b/src/TTImp/Elab/Term.idr
@@ -218,8 +218,7 @@ checkTerm rig elabinfo nest env (Implicit fc b) Nothing
                put EST (addBindIfUnsolved nm rig Explicit env metaval ty est)
          pure (metaval, gnf env ty)
 checkTerm rig elabinfo nest env (IWithUnambigNames fc ns rhs) exp
-    = with Core do
-         -- enter the scope -> add unambiguous names
+    = do -- enter the scope -> add unambiguous names
          est <- get EST
          rns <- resolveNames fc ns
          put EST $ record { unambiguousNames = mergeLeft rns (unambiguousNames est) } est