From 4eafa1c201eb851c98273d6d78377ce32586a658 Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 7 Oct 2010 12:44:02 +0000
Subject: test-suite: fix success/unification.v

This test it not relevant anyway, thanks to eta...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13513 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/unification.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index ddf122e853..e5b6e41598 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -135,4 +135,4 @@ Goal (forall (A B : Set) (f : A -> B), (fun x => f x) = f) ->
  forall (A B C : Set) (g : (A -> B) -> C) (f : A -> B), g (fun x => f x) = g f.
 Proof.
   intros.
-  rewrite H.
+  rewrite H with (f:=f0).
-- 
cgit v1.2.3