Merge pull request #33 from AeneasVerif/son_refactor

Update the code following Charon's refactor

1 files changed, 9 insertions, 9 deletions

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