From 8b27d81489121ddc4753a58135c1b6ccfdd70be6 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Fri, 25 Aug 2023 18:07:56 +0200
Subject: [PATCH] just use ticks here

---
 Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda
index 904b4372d9..40b434650d 100644
--- 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 ℓ''}