Cleanup + dump ttc version

idris-lang · Jul 5, 2023 · ad03731 · ad03731
1 parent 64b332b
commit ad03731
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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)