diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/coq/Primitives.v | 2 |
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 }. |