Bury some ⚰️ under the GpdCont.Experimental module tree

phijor · phijor · commit d677dd3f08e2 · 2025-01-08T19:27:48.000+02:00
diff --git a/GpdCont/Experimental/Coffin/Base.agda b/GpdCont/Experimental/Coffin/Base.agda
@@ -1,4 +1,4 @@
-module GpdCont.Coffin.Base where
+module GpdCont.Experimental.Coffin.Base where
 
 open import GpdCont.Prelude
 open import GpdCont.Experimental.Groups.Base
diff --git a/GpdCont/Experimental/Coffin/Eval.agda b/GpdCont/Experimental/Coffin/Eval.agda
@@ -1,6 +1,6 @@
-open import GpdCont.Coffin.Base
+open import GpdCont.Experimental.Coffin.Base
 
-module GpdCont.Coffin.Eval {ℓ} (C : Coffin ℓ) where
+module GpdCont.Experimental.Coffin.Eval {ℓ} (C : Coffin ℓ) where
 -- TODO: This should ideally do the following:
 -- import GpdCont.Coffin.GroupoidContainerInclusion as Inc
 -- open import GpdCont.GroupoidContainer.Eval (Inc.Coffin→GroupoidContainer C) public
diff --git a/GpdCont/Experimental/Coffin/GroupoidContainerInclusion.agda b/GpdCont/Experimental/Coffin/GroupoidContainerInclusion.agda
@@ -1,8 +1,8 @@
 open import GpdCont.Prelude
-open import GpdCont.Coffin.Base
+open import GpdCont.Experimental.Coffin.Base
 open import GpdCont.SymmetricContainer.Base
 
-module GpdCont.Coffin.GroupoidContainerInclusion {ℓ} (C : Coffin ℓ) where
+module GpdCont.Experimental.Coffin.GroupoidContainerInclusion {ℓ} (C : Coffin ℓ) where
 private
   module C = Coffin C
 
diff --git a/GpdCont/Experimental/Coffin/Lower.agda b/GpdCont/Experimental/Coffin/Lower.agda
@@ -1,7 +1,7 @@
 open import GpdCont.Prelude
-open import GpdCont.Coffin.Base
+open import GpdCont.Experimental.Coffin.Base
 
-module GpdCont.Coffin.Lower {ℓ} (C : Coffin ℓ) where
+module GpdCont.Experimental.Coffin.Lower {ℓ} (C : Coffin ℓ) where
   open import GpdCont.QuotientContainer.Base
   open import GpdCont.Equiv using (pathToEquivSym ; pathToEquivComp)
 

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-module GpdCont.Coffin.Base where`
	`1`	`+module GpdCont.Experimental.Coffin.Base where`
`2`	`2`
`3`	`3`	`open import GpdCont.Prelude`
`4`	`4`	`open import GpdCont.Experimental.Groups.Base`