Generalize instance declarations to any context, better name handling. Add hole kind info for topconstrs.

Derive eta_expansion from functional extensionality axiom.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10439 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 11 deletions

diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index 81bb5390b1..e890261e12 100644
--- a/theories/Program/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.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 *)
@@ -30,17 +31,6 @@ Proof.
   auto.
 Qed.
 
-(** Eta expansion *)
-
-Axiom eta_expansion_dep : forall A (B : A -> Type) (f : forall x : A, B x), 
-  f = fun x => f x.
-
-Lemma eta_expansion : forall A B (f : A -> B), 
-  f = fun x => f x.
-Proof.
-  intros ; apply eta_expansion_dep.
-Qed.
-
 (** Statements of functional equality for simple and dependent functions. *)
 
 Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), 
@@ -63,6 +53,22 @@ Tactic Notation "extensionality" ident(x) :=
     [ |- ?X = ?Y ] => apply (@fun_extensionality _ _ X Y) || apply (@fun_extensionality_dep _ _ X Y) ; intro x
   end.
 
+(** Eta expansion follows from extensionality. *)
+
+Lemma eta_expansion_dep : forall A (B : A -> Type) (f : forall x : A, B x), 
+  f = fun x => f x.
+Proof.
+  intros.
+  extensionality x.
+  reflexivity.
+Qed.
+  
+Lemma eta_expansion : forall A B (f : A -> B), 
+  f = fun x => f x.
+Proof.
+  intros ; apply eta_expansion_dep.
+Qed.
+
 (** The two following lemmas allow to unfold a well-founded fixpoint definition without
    restriction using the functional extensionality axiom. *)