Adding sections for definitions in change log

math-comp · Nov 10, 2015 · c5fd978 · c5fd978
1 parent 490d8fa
commit c5fd978
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/etc/ChangeLog b/etc/ChangeLog
@@ -18,13 +18,19 @@
 	  cfclass_transl -> cfclass_transr
 	  nontrivial_ideal -> proper_ideal
 	  zchar_orthonormalP -> vchar_orthonormalP
+
+	* Definitions that changed:
+	  seq_sub	
 
 	* Statements that changed:
 	  orbit_in_transl, orbit_sym, orbit_trans, orbit_transl, orbit_transr,
 	  cfAut_char, cfConjC_char, invg_lcosets, lcoset_transl,
 	  lcoset_transr, rcoset_transl, rcoset_transr, mem2_last,
 	  bind_unless, unless_contra, all_and2, all_and3, all_and4, all_and5,
 	  ltr0_neq0, ltr_prod, Zisometry_of_iso
+
+	* New definitions:
+	  adhoc_seq_sub_choiceMixin, adhoc_seq_sub_[choice|fin]Type
 
 	* New theorems:
 	  orbit_in_eqP, cards_draws, cfAut_lin_char, cfConjC_lin_char,