diff options
Diffstat (limited to 'tests/coq/misc/External_Opaque.v')
| -rw-r--r-- | tests/coq/misc/External_Opaque.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v index d2ee42d4..80be37e7 100644 --- a/tests/coq/misc/External_Opaque.v +++ b/tests/coq/misc/External_Opaque.v @@ -11,7 +11,7 @@ Import External_Types. Module External_Opaque. (** [core::mem::swap]: forward function *) -Axiom core_mem_swap_fwd : +Axiom core_mem_swap : forall(T : Type), T -> T -> state -> result (state * unit) . @@ -26,12 +26,12 @@ Axiom core_mem_swap_back1 : . (** [core::num::nonzero::NonZeroU32::{14}::new]: forward function *) -Axiom core_num_nonzero_non_zero_u32_new_fwd - : u32 -> state -> result (state * (option Core_num_nonzero_non_zero_u32_t)) +Axiom core_num_nonzero_NonZeroU32_new + : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t)) . (** [core::option::Option::{0}::unwrap]: forward function *) -Axiom core_option_option_unwrap_fwd : +Axiom core_option_Option_unwrap : forall(T : Type), option T -> state -> result (state * T) . |