From ae075db15638ee8878bebe3d31affb1aa320e90f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 28 May 2024 18:05:01 +0200
Subject: Reactivate the infinite-loop.rs test

---
 tests/coq/misc/InfiniteLoop.v | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 tests/coq/misc/InfiniteLoop.v

(limited to 'tests/coq')

diff --git a/tests/coq/misc/InfiniteLoop.v b/tests/coq/misc/InfiniteLoop.v
new file mode 100644
index 00000000..1c0ccbe0
--- /dev/null
+++ b/tests/coq/misc/InfiniteLoop.v
@@ -0,0 +1,27 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [infinite_loop] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module InfiniteLoop.
+
+(** [infinite_loop::bar]:
+    Source: 'tests/src/infinite-loop.rs', lines 4:0-4:8 *)
+Definition bar : result unit :=
+  Ok tt.
+
+(** [infinite_loop::foo]: loop 0:
+    Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 *)
+Fixpoint foo_loop (n : nat) : result unit :=
+  match n with | O => Fail_ OutOfFuel | S n1 => _ <- bar; foo_loop n1 end
+.
+
+(** [infinite_loop::foo]:
+    Source: 'tests/src/infinite-loop.rs', lines 6:0-6:8 *)
+Definition foo (n : nat) : result unit :=
+  foo_loop n.
+
+End InfiniteLoop.
-- 
cgit v1.2.3