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

1 files changed, 3 insertions, 8 deletions

diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index fb7f8827b..953296c28 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -25,17 +25,12 @@ Require Export Coq.Classes.SetoidClass.
 (* Application of the extensionality axiom to turn a goal on leibinz equality to 
    a setoid equivalence. *)
 
-Lemma setoideq_eq [ sa : Setoid a ] : forall x y : a, x == y -> x = y.
-Proof.
-  admit.
-Qed.
-
-Implicit Arguments setoideq_eq [[a] [sa]].
+Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
 
 (** Application of the extensionality principle for setoids. *)
 
-Ltac setoideq_ext :=
+Ltac setoid_extensionality :=
   match goal with
-    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y)
+    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
   end.