summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
authorSon Ho2023-08-08 17:50:16 +0200
committerSon Ho2023-08-08 17:50:16 +0200
commit77f309cec8e2f119272640083bc3476e4121952c (patch)
tree79451f2f2b2d5e26ab0ad067b0bfe3c598f58a29 /tests/coq/misc
parent6cdbb77f2be6f349729e2fd075ca3c51e9365b4f (diff)
Regenerate the test files
Diffstat (limited to 'tests/coq/misc')
-rw-r--r--tests/coq/misc/NoNestedBorrows.v18
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