From ad037317d32f660f571441ff6dbab512b6be8a8f Mon Sep 17 00:00:00 2001
From: Zoe Stafford <zoepolarsax@gmail.com>
Date: Wed, 5 Jul 2023 16:57:56 +0100
Subject: [PATCH] Cleanup + dump ttc version

---
 src/Core/Binary.idr       | 2 +-
 src/TTImp/Elab/Utils.idr  | 1 -
 src/TTImp/ProcessData.idr | 4 ++--
 3 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr
index be879de862..d9fc0a0565 100644
--- a/src/Core/Binary.idr
+++ b/src/Core/Binary.idr
@@ -29,7 +29,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 20230624 * 100 + 0
+ttcVersion = 20230705 * 100 + 0
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()
diff --git a/src/TTImp/Elab/Utils.idr b/src/TTImp/Elab/Utils.idr
index a734b3b3d9..cf7b57b2b1 100644
--- a/src/TTImp/Elab/Utils.idr
+++ b/src/TTImp/Elab/Utils.idr
@@ -39,7 +39,6 @@ detagSafe defs _ = pure False
 export
 isUnitType :
     {auto _ : Ref Ctxt Defs} ->
-    {vs : _} ->
     Term vs ->
     Core Bool
 isUnitType (Ref fc (TyCon {}) n) = do
diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr
index f75ac05993..afb176e7e1 100644
--- a/src/TTImp/ProcessData.idr
+++ b/src/TTImp/ProcessData.idr
@@ -247,7 +247,7 @@ findNewtype [con]
                  _ => Nothing
 findNewtype _ = pure ()
 
-hasArgs : {auto _ : Ref Ctxt Defs} -> {vs : _} -> Nat -> Term vs -> Core Bool
+hasArgs : {auto _ : Ref Ctxt Defs} -> Nat -> Term vs -> Core Bool
 hasArgs (S k) (Bind _ _ (Pi _ c _ ty) sc)
     = if isErased c || !(isUnitType ty)
         then hasArgs (S k) sc
@@ -277,7 +277,7 @@ typeCon (App _ fn _) = typeCon fn
 typeCon _ = Nothing
 
 shaped : {auto c : Ref Ctxt Defs} ->
-         ({vs : _} -> Term vs -> Core Bool) ->
+         (forall vs. Term vs -> Core Bool) ->
          List Constructor -> Core (Maybe Name)
 shaped as [] = pure Nothing
 shaped as (c :: cs)