- New auto hints for transparency/opacity control, not bound to

syntax yet. Doesn't change the auto/eauto behavior either.
- Typeclass resolution now considers everything transparent by 
default and does it consistently for "open" and closed terms.
- Correctly declare singleton classes definition as opaque for proof
search.
- Add a few initial declarations to make iff, id, compose... opaque
- Add definition of dependent signatures for dependent function types
and remove corresponding exception code in class_tactics. The 
instance requires higher-order unification and is not really usable yet.


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

4 files changed, 22 insertions, 7 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 22d9ff56f..03b0e9ad5 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -138,6 +137,6 @@ Program Instance pointwise_equivalence [ eqb : Equivalence B eqB ] :
 
   Next Obligation.
   Proof.
-    transitivity (y x0) ; auto.
+    transitivity (y a) ; auto.
   Qed.
 
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index dd082246c..5ac931033 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -20,6 +20,12 @@
 Tactic Notation "clapply" ident(c) :=
   eapply @c ; typeclasses eauto.
 
+(** Hints for the proof search: these combinators should be considered rigid. *)
+
+Require Import Program.Basics.
+
+Typeclasses Opaque id const flip compose arrow impl iff.
+
 (** The unconvertible typeclass, to test that two objects of the same type are 
    actually different. *)
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8acbe916b..270b9d8ac 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -75,10 +75,17 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop
 
 Open Local Scope signature_scope.
 
-(** Pointwise lifting is just respect with leibniz equality on the left. *)
+(** Dependent pointwise lifting of a relation on the range. *) 
+
+Definition forall_relation {A : Type} {B : A -> Type} (sig : Π a : A, relation (B a)) : relation (Π x : A, B x) :=
+  λ f g, Π a : A, sig a (f a) (g a).
+
+Arguments Scope forall_relation [type_scope type_scope signature_scope].
+
+(** Non-dependent pointwise lifting *)
 
 Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
-  fun f g => forall x : A, R (f x) (g x).
+  Eval compute in forall_relation (B:=λ _, B) (λ _, R).
 
 Lemma pointwise_pointwise A B (R : relation B) : 
   relation_equivalence (pointwise_relation R) (@eq A ==> R).
@@ -91,12 +98,14 @@ Hint Unfold Reflexive : core.
 Hint Unfold Symmetric : core.
 Hint Unfold Transitive : core.
 
+Typeclasses Opaque respectful pointwise_relation forall_relation.
+
 Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : 
   PER (A -> B) (R ==> R').
 
   Next Obligation.
   Proof with auto.
-    assert(R x0 x0). 
+    assert(R x0 x0).
     transitivity y0... symmetry...
     transitivity (y x0)...
   Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index bdd7b4b1d..dcf3139b2 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -23,12 +23,13 @@ Require Export Coq.Relations.Relation_Definitions.
 
 (** We allow to unfold the [relation] definition while doing morphism search. *)
 
-Typeclasses unfold relation.
-
 Notation inverse R := (flip (R:relation _) : relation _).
 
 Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
 
+(** Opaque for proof-search. *)
+Typeclasses Opaque complement.
+
 (** These are convertible. *)
 
 Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).