diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/misc/External_FunsExternal.v (renamed from tests/coq/misc/External_Opaque.v) | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_FunsExternal.v index b482431f..a8c5756a 100644 --- a/tests/coq/misc/External_Opaque.v +++ b/tests/coq/misc/External_FunsExternal.v @@ -7,8 +7,8 @@ Require Import List. Import ListNotations. Local Open Scope Primitives_scope. Require Export External_Types. -Import External_Types. -Module External_Opaque. +Include External_Types. +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. |