update import in cong and Utilities (#2732)

Author: jmougeot

src/Reflection/TCM/Utilities.agda

@@ -11,7 +11,7 @@ module Reflection.TCM.Utilities where
 open import Data.List using (List; []; _∷_; _++_; map)
 open import Data.Unit using (⊤; tt)
 open import Effect.Applicative using (RawApplicative; mkRawApplicative)
-open import Function using (case_of_)
+open import Function.Base using (case_of_)
 open import Reflection.AST.Meta using (Meta)
 open import Reflection.AST.Term using (Term)
 open import Reflection.TCM using (TC; pure; blockTC; blockerAll; blockerMeta)

src/Tactic/Cong.agda

@@ -26,21 +26,18 @@
 
 module Tactic.Cong where
 
-open import Function.Base using (_$_)
-
-open import Data.Bool.Base            using (true; false; if_then_else_; _∧_)
-open import Data.Char.Base   as Char  using (toℕ)
-open import Data.Float.Base  as Float using (_≡ᵇ_)
-open import Data.List.Base   as List  using ([]; _∷_)
-open import Data.Maybe.Base  as Maybe using (Maybe; just; nothing)
-open import Data.Nat.Base    as ℕ     using (ℕ; zero; suc; _≡ᵇ_; _+_)
-open import Data.Unit.Base            using (⊤)
-open import Data.Word64.Base   as Word64  using (toℕ)
-open import Data.Product.Base         using (_×_; map₁; _,_)
-open import Function                  using (flip; case_of_)
-
+open import Data.Bool.Base using (true; false; if_then_else_; _∧_)
+open import Data.Char.Base as Char using (toℕ)
+open import Data.Float.Base as Float using (_≡ᵇ_)
+open import Data.List.Base as List using ([]; _∷_)
+open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _≡ᵇ_; _+_)
+open import Data.Unit.Base using (⊤)
+open import Data.Word64.Base as Word64  using (toℕ)
+open import Data.Product.Base using (_×_; map₁; _,_)
+open import Function.Base using (_$_; flip; case_of_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
-open import Relation.Nullary.Decidable.Core            using (yes; no)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 
 -- 'Data.String.Properties' defines this via 'Dec', so let's use the
 -- builtin for maximum speed.