@@ -1014,6 +1014,8 @@ showImp impl tm = se 10 tm where
1014 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1014 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1015 se p (PPi (TacImp _ _ s _) n ty sc)
1015 se p (PPi (TacImp _ _ s _) n ty sc)
1016 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1016 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1018+ | Just str <- slist p e = str
1017 se p (PApp _ (PRef _ f) [])
1019 se p (PApp _ (PRef _ f) [])
1018 | not impl = show f
1020 | not impl = show f
1019 se p (PApp _ (PRef _ op@(UN (f:_))) args)
1021 se p (PApp _ (PRef _ op@(UN (f:_))) args)
@@ -1052,6 +1054,25 @@ showImp impl tm = se 10 tm where
1052 se p (PCoerced t) = se p t
1054 se p (PCoerced t) = se p t
1053-- se p x = "Not implemented"
1055-- se p x = "Not implemented"
1057+ slist' p (PApp _ (PRef _ nil) _)
1058+ | nsroot nil == UN "Nil" = Just []
1059+ slist' p (PApp _ (PRef _ cons) args)
1060+ | nsroot cons == UN "::",
1061+ (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1063+ Just tl' <- slist' p tl
1066+ isImp (PImp {}) = True
1068+ slist' _ _ = Nothing
1070+ slist p e | Just es <- slist' p e = Just $
1071+ case es of [] -> "[]"
1072+ [x] -> "[" ++ se p x ++ "]"
1073+ xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
1074+ slist _ _ = Nothing
1055 sArg (PImp _ _ n tm _) = siArg (n, tm)
1076 sArg (PImp _ _ n tm _) = siArg (n, tm)
1056 sArg (PExp _ _ tm _) = seArg tm
1077 sArg (PExp _ _ tm _) = seArg tm
1057 sArg (PConstraint _ _ tm _) = scArg tm
1078 sArg (PConstraint _ _ tm _) = scArg tm