From 7e266b7cec70ab175d082d6a3398f20554ec8e5e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Dec 2004 12:10:32 +0000
Subject: Ajout test bug 860

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6513 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Fixpoint.out8 |  5 +++++
 test-suite/output/Fixpoint.v8   | 11 ++++++++++-
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/test-suite/output/Fixpoint.out8 b/test-suite/output/Fixpoint.out8
index 4dca551a0f..5af28a5aff 100644
--- a/test-suite/output/Fixpoint.out8
+++ b/test-suite/output/Fixpoint.out8
@@ -4,3 +4,8 @@ list B := match l with
           | a :: l0 => f a :: F A B f l0
           end
      : forall A B : Set, (A -> B) -> list A -> list B
+let fix f (m : nat) : nat := match m with
+                             | O => 0
+                             | S m' => f m'
+                             end in f 0
+     : nat
diff --git a/test-suite/output/Fixpoint.v8 b/test-suite/output/Fixpoint.v8
index 09d5405fc8..ab1467a561 100644
--- a/test-suite/output/Fixpoint.v8
+++ b/test-suite/output/Fixpoint.v8
@@ -5,4 +5,13 @@ Check
    list B := match l with
              | nil => nil
              | a :: l => f a :: F _ _ f l
-             end).
\ No newline at end of file
+             end).
+
+(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf bug #860) *)
+Check
+  let fix f (m : nat) : nat :=
+    match m with
+    | O => 0
+    | S m' => f m'
+    end
+  in f 0.
-- 
cgit v1.2.3