Merge pull request #64 from AeneasVerif/son/merge_back

Merge the forward/backward functions

1 files changed, 4 insertions, 16 deletions

diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 31e69c39..6773ac18 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -11,31 +11,19 @@ Require Import External_Types.
 Include External_Types.
 Module External_FunsExternal_Template.
 
-(** [core::mem::swap]: forward function
+(** [core::mem::swap]:
     Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
 Axiom core_mem_swap :
-  forall(T : Type), T -> T -> state -> result (state * unit)
+  forall(T : Type), T -> T -> state -> result (state * (T * T))
 .
 
-(** [core::mem::swap]: backward function 0
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-Axiom core_mem_swap_back0 :
-  forall(T : Type), T -> T -> state -> state -> result (state * T)
-.
-
-(** [core::mem::swap]: backward function 1
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-Axiom core_mem_swap_back1 :
-  forall(T : Type), T -> T -> state -> state -> result (state * T)
-.
-
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
+(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
     Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
 Axiom core_num_nonzero_NonZeroU32_new
   : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
 .
 
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+(** [core::option::{core::option::Option<T>}::unwrap]:
     Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
 Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)