@@ -147,22 +147,22 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm
147147 = PLam un n NoFC (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) [] sc)
148148 de tys env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)
149149 | toplevel_imp impl -- information in 'imps' repeated
150− = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC
150+ = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC
151151 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
152152 de tys env is (Bind n (Pi rig (Just impl) ty _) sc)
153153 | tcimplementation impl
154− = PPi constraint n NoFC (de tys env [] ty)
154+ = PPi constraint n NoFC (de tys env [] ty)
155155 (de ((n, ty) : tys) ((n,n):env) is sc)
156156 | otherwise
157157 = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de tys env [] ty) (de tys ((n,n):env) is sc)
158158 de tys env ((PImp { argopts = opts }):is) (Bind n (Pi rig _ ty _) sc)
159− = PPi (Imp opts Dynamic False Nothing False rig) n NoFC
159+ = PPi (Imp opts Dynamic False Nothing False rig) n NoFC
160160 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
161161 de tys env (PConstraint _ _ _ _:is) (Bind n (Pi rig _ ty _) sc)
162− = PPi (constraint { pcount = rig}) n NoFC
162+ = PPi (constraint { pcount = rig}) n NoFC
163163 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
164164 de tys env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi rig _ ty _) sc)
165− = PPi ((tacimpl tac) { pcount = rig }) n NoFC
165+ = PPi ((tacimpl tac) { pcount = rig }) n NoFC
166166 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
167167 de tys env (plic:is) (Bind n (Pi rig _ ty _) sc)
168168 = PPi (Exp (argopts plic) Dynamic False rig)
@@ -170,7 +170,7 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm
170170 (de tys env [] ty)
171171 (de ((n, ty) : tys) ((n,n):env) is sc)
172172 de tys env [] (Bind n (Pi rig _ ty _) sc)
173− = PPi (expl { pcount = rig }) n NoFC (de tys env [] ty)
173+ = PPi (expl { pcount = rig }) n NoFC (de tys env [] ty)
174174 (de ((n, ty) : tys) ((n,n):env) [] sc)
175175
176176 de tys env imps (Bind n (Let ty val) sc)
@@ -179,7 +179,7 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm
179179 , (P _ cOp _, args) <- unApply sc
180180 , Just caseblock <- delabCase tys env imps val cOp args = caseblock
181181 | otherwise =
182− PLet un n NoFC (de tys env [] ty)
182+ PLet un n NoFC (de tys env [] ty)
183183 (de tys env [] val) (de ((n, ty) : tys) ((n,n):env) [] sc)
184184 de tys env _ (Bind n (Hole ty) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc
185185 de tys env _ (Bind n (Guess ty val) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc
@@ -235,10 +235,10 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm
235235 | Just imps <- lookupCtxtExact n (idris_implicits ist)
236236 = PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)
237237 | otherwise = PApp un (PRef un [] n) (map pexp args)
238− where
239− findImp (Bind n (Pi _ im@(Just i) _ _) sc)
238+ where
239+ findImp (Bind n (Pi _ im@(Just i) _ _) sc)
240240 = pimp n Placeholder True : findImp sc
241− findImp (Bind n (Pi _ _ _ _) sc)
241+ findImp (Bind n (Pi _ _ _ _) sc)
242242 = pexp Placeholder : findImp sc
243243 findImp _ = []
244244 imp (PImp p m l n _) arg = PImp p m l n arg