docs(NearlyConstant): remove comments that no longer apply

RedPRL · Nov 21, 2023 · 065659a · 065659a
1 parent 097e67f
commit 065659a
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/src/Mugen/Algebra/Displacement/NearlyConstant.agda b/src/Mugen/Algebra/Displacement/NearlyConstant.agda
@@ -76,12 +76,6 @@ module NearlyConst
 
   --------------------------------------------------------------------------------
   -- Compactness Predicate
-  --
-  -- This is defined as a recursive family to avoid
-  -- frustrating situations with indexed types + cubical.
-  -- Furthermore, we avoid with-abstraction for things
-  -- that we actually want to compute: Agda can get
-  -- very confused if we do that!
 
   -- A list is compact relative to a base 'b' if it has
   -- no trailing b's.