Add reminder.

FEM/Algebra/MonoidComp.v

@@ -306,7 +306,8 @@ Variable f : '(E -> E)^n.
 Variable j : 'I_n.+1.
 Hypothesis Hf : forall i, funS PE PE (widenF (leq_ord j) f i).
 
-(* TODO FC (15/12/2023): factor these proofs, and probably others too... *)
+(* TO BE REMOVED FOR PUBLICATION!
+ TODO FC (15/12/2023): factor these proofs, and probably others too... *)
 
 Lemma comp_n_part_f_plus_compat_sub :
   (forall i, f_plus_compat_sub PE (widenF (leq_ord j) f i)) ->
@@ -406,7 +407,8 @@ Variable f : '(E -> E)^n.
 Variable j : 'I_n.+1.
 Hypothesis Hf : forall i, funS PE PE (widenF (leq_ord j) f i).
 
-(* TODO FC (15/12/2023): factor these proofs, and probably others too... *)
+(* TO BE REMOVED FOR PUBLICATION!
+ TODO FC (15/12/2023): factor these proofs, and probably others too... *)
 
 Lemma comp_n_part_morphism_g_sub :
   (forall i, morphism_g_sub PE (widenF (leq_ord j) f i)) ->
@@ -511,7 +513,8 @@ Variable f : '(E -> E)^n.
 Variable j : 'I_n.+1.
 Hypothesis Hf : forall i, funS PE PE (widenF (leq_ord j) f i).
 
-(* TODO FC (15/12/2023): factor these proofs, and probably others too... *)
+(* TO BE REMOVED FOR PUBLICATION!
+ TODO FC (15/12/2023): factor these proofs, and probably others too... *)
 
 Lemma comp_n_part_f_scal_compat_sub :
   (forall i, f_scal_compat_sub PE (widenF (leq_ord j) f i)) ->