@@ -796,17 +796,20 @@ implicit' syn ignore n ptm
796 return tm'
796 return tm'
798implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
798implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
799−implicitise syn ignore ist tm
799+implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
800− = let (declimps, ns') = execState (imps True [] tm) ([], [])
800+ let (declimps, ns') = execState (imps True [] tm) ([], [])
801 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
801 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
802− ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
802+ ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
803+ nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
803 if null ns
804 if null ns
804 then (tm, reverse declimps)
805 then (tm, reverse declimps)
805− else implicitise syn ignore ist (pibind uvars ns tm)
806+ else implicitise syn ignore ist (pibind uvars nsOrder tm)
807 uvars = map ipair (filter uimplicit (using syn))
808 uvars = map ipair (filter uimplicit (using syn))
808 pvars = syn_params syn
809 pvars = syn_params syn
811+ inUsing n = n `elem` map fst uvars
810 ipair (UImplicit x y) = (x, y)
813 ipair (UImplicit x y) = (x, y)
811 uimplicit (UImplicit _ _) = True
814 uimplicit (UImplicit _ _) = True
812 uimplicit _ = False
815 uimplicit _ = False