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

2 files changed, 14 insertions, 7 deletions

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 3040dd04ba..8a3e5dccd9 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -18,7 +19,7 @@ Unset Strict Implicit.
 
 Require Export Coq.Program.FunctionalExtensionality.
 
-Notation  "'λ' x : T , y" := (fun x:T => y) (at level 1, x,T,y at level 10) : program_scope.
+Notation  " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope.
 
 Open Scope program_scope.
 
@@ -45,7 +46,7 @@ Proof.
 Qed.
 
 Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), 
-  h ∘ (g ∘ f) = h ∘ g ∘ f.
+  h ∘ g ∘ f = h ∘ (g ∘ f).
 Proof.
   intros.
   reflexivity.
@@ -117,7 +118,7 @@ Qed.
 
 (** Useful implicits and notations for lists. *)
 
-Require Export Coq.Lists.List.
+Require Import Coq.Lists.List.
 
 Implicit Arguments nil [[A]].
 Implicit Arguments cons [[A]].
@@ -141,3 +142,9 @@ Tactic Notation "exist" constr(x) := exists x.
 Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
 Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
 Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
+
+(* Notation " 'Σ' x : T , p" := (sigT (fun x : T => p)) *)
+(*   (at level 200, x ident, y ident, right associativity) : program_scope. *)
+
+(* Notation " 'Π' x : T , p " := (forall x : T, p) *)
+(*   (at level 200, x ident, right associativity) : program_scope. *)
\ No newline at end of file
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 70b1b1b5a2..98b18f9030 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -17,7 +17,7 @@ Section Well_founded.
     
     Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
       F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y) 
-        (Acc_inv r (proj1_sig y) (proj2_sig y))).
+        (Acc_inv r (proj2_sig y))).
     
     Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
   End Acc.
@@ -38,7 +38,7 @@ Section Well_founded.
 
     Lemma Fix_F_eq :
       forall (x:A) (r:Acc R x),
-        F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r.
+        F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r.
     Proof. 
       destruct r using Acc_inv_dep; auto.
     Qed.
@@ -89,7 +89,7 @@ Section Well_founded_measure.
     
     Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
       F_sub x (fun y: { y : A | m y < m x}  => Fix_measure_F_sub (proj1_sig y) 
-        (Acc_inv r (m (proj1_sig y)) (proj2_sig y))).
+        (@Acc_inv _ _ _ r (m (proj1_sig y)) (proj2_sig y))).
     
     Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
   
@@ -111,7 +111,7 @@ Section Well_founded_measure.
 
     Lemma Fix_measure_F_eq :
       forall (x:A) (r:Acc lt (m x)),
-        F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (proj2_sig y))) = Fix_F x r.
+        F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r.
     Proof.
       intros x.
       set (y := m x).