From 77f309cec8e2f119272640083bc3476e4121952c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 8 Aug 2023 17:50:16 +0200
Subject: Regenerate the test files

---
 tests/coq/misc/NoNestedBorrows.v | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'tests/coq/misc')

diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index f93254e1..c1c24e00 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -238,23 +238,23 @@ Definition test_char_fwd : result char :=
   Return (char_of_byte Coq.Init.Byte.x61)
 .
 
-(** [no_nested_borrows::NodeElem] *)
-Inductive Node_elem_t (T : Type) :=
-| NodeElemCons : Tree_t T -> Node_elem_t T -> Node_elem_t T
-| NodeElemNil : Node_elem_t T
-
 (** [no_nested_borrows::Tree] *)
-with Tree_t (T : Type) :=
+Inductive Tree_t (T : Type) :=
 | TreeLeaf : T -> Tree_t T
 | TreeNode : T -> Node_elem_t T -> Tree_t T -> Tree_t T
-.
 
-Arguments NodeElemCons {T} _ _.
-Arguments NodeElemNil {T}.
+(** [no_nested_borrows::NodeElem] *)
+with Node_elem_t (T : Type) :=
+| NodeElemCons : Tree_t T -> Node_elem_t T -> Node_elem_t T
+| NodeElemNil : Node_elem_t T
+.
 
 Arguments TreeLeaf {T} _.
 Arguments TreeNode {T} _ _ _.
 
+Arguments NodeElemCons {T} _ _.
+Arguments NodeElemNil {T}.
+
 (** [no_nested_borrows::list_length]: forward function *)
 Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 :=
   match l with
-- 
cgit v1.2.3