fixed changelog

math-comp · Oct 1, 2024 · 970a421 · 970a421
1 parent 725ec83
commit 970a421
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -24,16 +24,18 @@
 - in `measure.v`:
   + lemma `measurable_fun_set1`
 - in file `classical_orders.v`,
-  + new definitions `share_prefix`, `first_diff`, `lexi_bigprod`, `start_with`,
+  + new definitions `same_prefix`, `first_diff`, `lexi_bigprod`, `start_with`,
     `big_lexi_order`, and `big_lexi_ord`.
-  + new lemmas `share_prefix0`, `share_prefixC`, `share_prefixS`,
-    `share_prefix_refl`, `share_prefix_trans`, `first_diffC`,
+  + new lemmas `same_prefix0`, `same_prefix_sym`, `same_prefix_leq`,
+    `same_prefix_refl`, `same_prefix_trans`, `first_diff_sym`,
     `first_diff_unique`, `first_diff_SomeP`, `first_diff_NoneP`,
     `first_diff_lt`, `first_diff_eq`, `first_diff_dfwith`,
     `lexi_bigprod_reflexive`, `lexi_bigprod_anti`, `lexi_bigprod_trans`,
     `lexi_bigprod_total`, `start_with_prefix`, `lexi_bigprod_prefix_lt`,
     `lexi_bigprod_prefix_gt`, `lexi_bigprod_between`,
-    `big_lexi_interval_prefix`, and `shared_prefix_closed_itv`.
+    `big_lexi_interval_prefix`, and `same_prefix_closed_itv`.
+
+
 
 ### Changed