From 37e8a0f5ff7d964eb9525fef765b38e44f79302b Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 15:48:27 +0200
Subject: Update test outputs

---
 tests/fstar/misc/External.Funs.fst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/fstar/misc/External.Funs.fst')

diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 5a7a9f32..18fc901f 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -15,12 +15,12 @@ let core_marker_CopyU32 : core_marker_Copy_t u32 = {
 }
 
 (** [external::use_get]:
-    Source: 'tests/src/external.rs', lines 5:0-5:37 *)
+    Source: 'tests/src/external.rs', lines 8:0-8:37 *)
 let use_get (rc : core_cell_Cell_t u32) (st : state) : result (state & u32) =
   core_cell_Cell_get u32 core_marker_CopyU32 rc st
 
 (** [external::incr]:
-    Source: 'tests/src/external.rs', lines 9:0-9:31 *)
+    Source: 'tests/src/external.rs', lines 12:0-12:31 *)
 let incr
   (rc : core_cell_Cell_t u32) (st : state) :
   result (state & (core_cell_Cell_t u32))
-- 
cgit v1.2.3


From e288482f437a5f259be5f81eb996b5b28158b300 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 16:51:03 +0200
Subject: Update output files

---
 tests/fstar/misc/External.Funs.fst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/fstar/misc/External.Funs.fst')

diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 18fc901f..f5e8d4b7 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -15,12 +15,12 @@ let core_marker_CopyU32 : core_marker_Copy_t u32 = {
 }
 
 (** [external::use_get]:
-    Source: 'tests/src/external.rs', lines 8:0-8:37 *)
+    Source: 'tests/src/external.rs', lines 9:0-9:37 *)
 let use_get (rc : core_cell_Cell_t u32) (st : state) : result (state & u32) =
   core_cell_Cell_get u32 core_marker_CopyU32 rc st
 
 (** [external::incr]:
-    Source: 'tests/src/external.rs', lines 12:0-12:31 *)
+    Source: 'tests/src/external.rs', lines 13:0-13:31 *)
 let incr
   (rc : core_cell_Cell_t u32) (st : state) :
   result (state & (core_cell_Cell_t u32))
-- 
cgit v1.2.3