just use ticks here

agda · Aug 25, 2023 · 8b27d81 · 8b27d81
1 parent 8f48f7d
commit 8b27d81
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda
@@ -52,7 +52,7 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where
   open C using (var; const)
 
   {-
-    Construction of the elimProp eliminator.
+    Construction of the 'elimProp' eliminator.
   -}
   module _
     {P : ⟨ R [ I ] ⟩ → Type ℓ''}