Fix the models for core::mem::replace

1 files changed, 1 insertions, 1 deletions

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 }.