From 6efaa1f45a855418d0bc7c8656e4ed83778903ee Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 25 Aug 2007 15:44:39 +0000
Subject: Extension et documentation de real_clean/evar_define dans
 evarutil.ml: l'unification sait maintenant résoudre des équations du genre
 "?n[...;x:=?m[...;y:=t;...]] = t" lorsque x et y sont uniques vérifiant cette
 propriété (la solution est alors de poser ?m:=y et ?n:=x); le type de t est
 aussi pris en compte dans cette situation (ce genre de problème permet de
 résoudre des cas simples d'unification avec dépendance: cf l'exemple de
 foldrn dans test-suite/success/Fixpoint.v)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10092 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Fixpoint.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index 680046da4c..bc9c8a374b 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 even in presence of (non ambiguous)
+   dependencies (needs revision ) *)
+
+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.
+
-- 
cgit v1.2.3