diff options
| author | Son Ho | 2023-11-27 09:37:31 +0100 |
|---|---|---|
| committer | Son Ho | 2023-11-27 09:37:31 +0100 |
| commit | 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc (patch) | |
| tree | 3bdc3f7fb87fe53140156eabe35eaee2e7e2f704 /tests/coq/misc/External_FunsExternal.v | |
| parent | d84040e000333d6d2a212fb849a38fb73a65eb48 (diff) | |
Update the generation of files for external definitions and regenerate the tests
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/misc/External_FunsExternal.v (renamed from tests/coq/misc/External_Opaque.v) | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_FunsExternal.v index b482431f..07d43061 100644 --- a/tests/coq/misc/External_Opaque.v +++ b/tests/coq/misc/External_FunsExternal.v @@ -8,7 +8,7 @@ Import ListNotations. Local Open Scope Primitives_scope. Require Export External_Types. Import External_Types. -Module External_Opaque. +Module External_FunsExternal. (** [core::mem::swap]: forward function Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) @@ -40,4 +40,4 @@ Axiom core_option_Option_unwrap : forall(T : Type), option T -> state -> result (state * T) . -End External_Opaque . +End External_FunsExternal. |