Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index 680046da..cf821073 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -29,3 +29,22 @@ CoFixpoint g (n:nat) (m:=pred n) (l:Stream m) (p:=S n) : Stream p :=
 
 Eval compute in (fun l => match g 2 (Consn 0 6 l) with Consn _ a _ => a end).
 
+(* Check inference of simple types in presence of non ambiguous
+   dependencies (needs revision 10125) *)
+
+Section folding.
+
+Inductive vector (A:Type) : nat -> Type :=
+  | Vnil : vector A 0
+  | Vcons : forall (a:A) (n:nat), vector A n -> vector A (S n).
+
+Variables (B C : Set) (g : B -> C -> C) (c : C).
+
+Fixpoint foldrn n bs :=
+  match bs with
+  | Vnil => c
+  | Vcons b _ tl => g b (foldrn _ tl)
+  end.
+
+End folding.
+