diff options
| author | Son Ho | 2023-11-27 10:29:25 +0100 |
|---|---|---|
| committer | Son Ho | 2023-11-27 10:29:25 +0100 |
| commit | bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 (patch) | |
| tree | b491462e77665dceb44b4899f97508d440c57d6a /tests/coq/array | |
| parent | 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc (diff) | |
Generate a dedicated file for the external types
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/array/Array.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/coq/array/Array.v b/tests/coq/array/Array.v index 99ff3b03..105ce21f 100644 --- a/tests/coq/array/Array.v +++ b/tests/coq/array/Array.v @@ -528,4 +528,4 @@ Definition ite : result unit := Return tt . -End Array . +End Array. |