From 01c65fbba132653bcf66724e8e01b5d5038ea3b1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Sun, 9 Mar 2025 14:53:15 +0100
Subject: [PATCH] Done.
---
Algebra/Monoid/Monoid_FF.v | 3 ---
1 file changed, 3 deletions(-)
diff --git a/Algebra/Monoid/Monoid_FF.v b/Algebra/Monoid/Monoid_FF.v
index 4a01c039..6bf70163 100644
--- a/Algebra/Monoid/Monoid_FF.v
+++ b/Algebra/Monoid/Monoid_FF.v
@@ -114,9 +114,6 @@ Section Monoid_FF_Def.
Context {G : AbelianMonoid}.
-(* FIXME: COMMENTS TO BE REMOVED FOR PUBLICATION!
- TODO FC (07/03/2025): make partial applications abbreviations. *)
-
Definition itemF n i0 x : 'G^n := replaceF i0 x 0.
Definition squeezeF {n} (i0 i1 : 'I_n.+1) : 'G^n.+1 -> 'G^n :=
--
GitLab