From d081dcfaedb5b7e2ad78574a053bcebc4bfb564a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 26 Feb 2008 15:58:32 +0000
Subject: Proper implicit arguments handling for assumptions
 (Axiom/Variable...). New tactic clapply to apply unapplied class methods in
 tactic mode, simple solution to the fact that apply does not work up-to
 classes yet. Add Functions.v for class definitions related to functional
 morphisms.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10589 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Wf.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Init')

diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 6e07ea43a9..87cd9becc0 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -157,7 +157,7 @@ Section Well_founded_2.
    P x x' :=
     F
       (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
-         Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)).
+         Acc_iter_2 (x:=y) (x':=y') (Acc_inv a h)).
   End Acc_iter_2.
 
   Hypothesis Rwf : well_founded R.
-- 
cgit v1.2.3