summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2023-10-27 13:34:03 +0200
committerSon Ho2023-10-27 13:34:03 +0200
commit49117ba254679f98938223711810191c3f7d788f (patch)
tree2a29b2be5becbb90104c552b77b4f9d3b3fa2546 /backends
parent1c55079dac0c51e45f7d77c67bfdbdb8c52ed192 (diff)
Regenerate the Coq test files
Diffstat (limited to '')
-rw-r--r--backends/coq/Primitives.v2
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).