1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output/Fixpoint.v8 b/test-suite/output/Fixpoint.v8
new file mode 100644
index 000000000..09d5405fc
--- /dev/null
+++ b/test-suite/output/Fixpoint.v8
@@ -0,0 +1,8 @@
+Require Import List.
+
+Check
+  (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : 
+   list B := match l with
+             | nil => nil
+             | a :: l => f a :: F _ _ f l
+             end).
+\ No newline at end of file