Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 17 insertions, 6 deletions

diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 270fff4e..fc27e8d2 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -1,7 +1,18 @@
-Require PolyList.
+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).
+
+(* 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.
 
-Check Fix F { F/4 : (A,B:Set)(A->B)->(list A)->(list B) :=
- [_,_,f,l]Cases l of
-   nil => (nil ?)
- | (cons a l) => (cons (f a) (F ? ? f l))
- end}.