From 5be6c5a1c57486de03cd9a6823196ed4b04fab4c Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 28 Jun 2024 09:29:04 +0200 Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1223 --- theories/initctree.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/initctree.v b/theories/initctree.v index 6e8f690..d7bd7d9 100644 --- a/theories/initctree.v +++ b/theories/initctree.v @@ -105,7 +105,7 @@ Lemma ctree_add_dyck_leaf_of m n d : Proof. elim: n m d => [|n IHn] m /=; first by rewrite addn0 gen_dyck_all_close. elim: m => [|m IHm] d; rewrite doubleS /=; first by rewrite addn0 IHn. -by rewrite IHm IHn doubleS addnA -addnE !addnS. +by rewrite IHm IHn doubleS addnA -?addnE !addnS. (* TODO: remove ?addnE when requiring Coq >= 8.21 *) Qed. Lemma ctree_leaf_table_size h : size (ctree_leaf_table h) = h.+1.