From e4542668e6d348e0300e76bb77105af24aff4233 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 19 Apr 2021 19:08:08 +0200
Subject: Use List.repeat from Coq's standard library instead of list_repeat

---
 backend/NeedDomain.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index fc1ae16d..62b8ff90 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -737,7 +737,7 @@ Lemma store_argument_sound:
 Proof.
   intros.
   assert (UNDEF: list_forall2 memval_lessdef
-                     (list_repeat (size_chunk_nat chunk) Undef)
+                     (List.repeat Undef (size_chunk_nat chunk))
                      (encode_val chunk w)).
   {
      rewrite <- (encode_val_length chunk w).
-- 
cgit