diff options
| author | Son Ho | 2023-10-27 13:34:03 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-27 13:34:03 +0200 |
| commit | 49117ba254679f98938223711810191c3f7d788f (patch) | |
| tree | 2a29b2be5becbb90104c552b77b4f9d3b3fa2546 /backends/coq | |
| parent | 1c55079dac0c51e45f7d77c67bfdbdb8c52ed192 (diff) | |
Regenerate the Coq test files
Diffstat (limited to 'backends/coq')
| -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 8e0e973d..85e38f01 100644 --- a/backends/coq/Primitives.v +++ b/backends/coq/Primitives.v @@ -499,7 +499,7 @@ Qed. Axiom mk_array : forall (T : Type) (n : usize) (l : list T), array T n. (* For initialization *) -Axiom array_repeat : forall {T : Type} (n : usize) (x : T), array T n. +Axiom array_repeat : forall (T : Type) (n : usize) (x : T), array T n. Axiom array_index_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. Axiom array_update_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n). |