diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-07 12:44:02 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-07 12:44:02 +0000 |
| commit | 4eafa1c201eb851c98273d6d78377ce32586a658 (patch) | |
| tree | 1b4b167109df809a45eed40ba668a9855117087d | |
| parent | c83eef69abcb41b8889c9b36ef42fb7aac2307cb (diff) | |
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
| -rw-r--r-- | test-suite/success/unification.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index ddf122e85..e5b6e4159 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). |