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

1 files changed, 19 insertions, 0 deletions

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.
+