From d9ace7d5f1968f26b586fb712c725b2ce51086f8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 21:50:11 +0100
Subject: Fix the models for core::mem::replace

---
 backends/coq/Primitives.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backends/coq')

diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index c0056073..e6d3118f 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -67,7 +67,7 @@ Definition string := Coq.Strings.String.string.
 Definition char := Coq.Strings.Ascii.ascii.
 Definition char_of_byte := Coq.Strings.Ascii.ascii_of_byte.
 
-Definition core_mem_replace (a : Type) (x : a) (y : a) : a * (a -> a) := (x, fun x => x) .
+Definition core_mem_replace (a : Type) (x : a) (y : a) : a * a := (x, x) .
 
 Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }.
 Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }.
-- 
cgit v1.2.3