diff options
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). |