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/misc/PoloniusList.v | |
| parent | 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc (diff) | |
Generate a dedicated file for the external types
Diffstat (limited to 'tests/coq/misc/PoloniusList.v')
| -rw-r--r-- | tests/coq/misc/PoloniusList.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v index a0820e40..2371b1cc 100644 --- a/tests/coq/misc/PoloniusList.v +++ b/tests/coq/misc/PoloniusList.v @@ -41,4 +41,4 @@ Fixpoint get_list_at_x_back end . -End PoloniusList . +End PoloniusList. |