Rename Reflection.TCMonadSyntax to Reflection.TypeChecking.MonadSyntax (#1115)

Author: MatthewDaggitt

CHANGELOG.md

@@ -383,8 +383,8 @@ New modules
   Reflection.Meta
   Reflection.Name
   Reflection.Pattern
-  Reflection.TCMonadSyntax
   Reflection.Term
+  Reflection.TypeChecking.MonadSyntax
   ```
 
 * New tactics for monoid and ring solvers. See `README.Tactic.MonoidSolver/RingSolver` for details

src/Reflection.agda

@@ -71,7 +71,7 @@ open Builtin public
 
 -- Standard monad operators
 
-open import Reflection.TCMonadSyntax public
+open import Reflection.TypeChecking.MonadSyntax public
   using (_>>=_; _>>_)
 
 newMeta : Type → TC Term

src/Reflection/TCMonadSyntax.agda renamed to src/Reflection/TypeChecking/MonadSyntax.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Reflection.TCMonadSyntax where
+module Reflection.TypeChecking.MonadSyntax where
 
 open import Agda.Builtin.Reflection
 open import Level using (Level)

src/Tactic/MonoidSolver.agda

@@ -82,9 +82,9 @@ open import Data.Nat     as ℕ       using (ℕ; suc; zero)
 open import Data.Product as Product using (_×_; _,_)
 
 open import Agda.Builtin.Reflection
-open import Reflection.TCMonadSyntax
-open import Reflection.Term using (getName; _⋯⟅∷⟆_)
 open import Reflection.Argument
+open import Reflection.Term using (getName; _⋯⟅∷⟆_)
+open import Reflection.TypeChecking.MonadSyntax
 
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 

src/Tactic/RingSolver.agda

@@ -23,9 +23,9 @@ open import Data.Unit           using (⊤)
 open import Data.String         using (String)
 open import Data.Product        using (_,_)
 open import Function
-open import Reflection.TCMonadSyntax
 open import Reflection.Argument
 open import Reflection.Term
+open import Reflection.TypeChecking.MonadSyntax
 
 open import Tactic.RingSolver.NonReflective renaming (solve to solve-fn)
 open import Tactic.RingSolver.Core.AlmostCommutativeRing