Minor fixes. Use expanded type in class_tactics for Morphism search, to

alleviate some problems with delta. Better precedence in lambda
notation. Temporarily deactivate notations for relation conjunction,
equivalence and so on, while we search for a better syntax and maybe a
generalization (fixes bug #1820). Better destruct_call in
Program.Tactics.


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

6 files changed, 54 insertions, 39 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 5c24224774..32103a0581 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -580,7 +580,7 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars
     let appmtype = Typing.type_of env sigma appm in
     let cstrs = List.map (function None -> None | Some (_, (a, r, _, _)) -> Some (a, r)) (Array.to_list morphobjs') in
     let appmtype', signature, sigargs = build_signature evars env appmtype cstrs cstr (fun (a, r) -> r) in
-    let cl_args = [| appmtype ; signature ; appm |] in
+    let cl_args = [| appmtype' ; signature ; appm |] in
     let app = mkApp (Lazy.force morphism_type, cl_args) in
     let morph = Evarutil.e_new_evar evars env app in
     let proj = 
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 0d71df82f3..b625eb151a 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -478,3 +478,9 @@ match l return l = l with
     end
 | _ => refl_equal _
 end.
+
+Fixpoint app {A} {n m} (v : listn A n) (w : listn A m) : listn A (n + m) :=
+  match v with
+    | niln => w
+    | consn a n' v' => consn _ a _ (app v' w)
+  end.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 3a029371b4..d10cb97242 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -20,8 +20,6 @@ Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
-Open Local Scope relation_scope.
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -447,7 +445,7 @@ Proof.
 Qed.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
-  inverse (R ==> R') <R> (inverse R ==> inverse R').
+  relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R').
 Proof.
   intros.
   unfold flip, respectful.
@@ -593,5 +591,5 @@ Program Instance {A : Type} => all_inverse_impl_morphism :
   Qed.
 
 Lemma inverse_pointwise_relation A (R : relation A) : 
-  pointwise_relation (inverse R) <R> inverse (pointwise_relation (A:=A) R).
+  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
 Proof. reflexivity. Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 6ef2f756d3..f5d3cc1c45 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -217,26 +217,24 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid
 Definition relation_equivalence {A : Type} : relation (relation A) :=
   fun (R R' : relation A) => forall x y, R x y <-> R' x y.
 
-Infix "<R>" := relation_equivalence (at level 95, no associativity) : relation_scope.
-
 Class subrelation {A:Type} (R R' : relation A) :=
   is_subrelation : forall x y, R x y -> R' x y.
 
 Implicit Arguments subrelation [[A]].
 
-Infix "-R>" := subrelation (at level 70) : relation_scope.
 
 Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
   fun x y => R x y /\ R' x y.
 
-Infix "/R\" := relation_conjunction (at level 80, right associativity) : relation_scope.
-
 Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
   fun x y => R x y \/ R' x y.
 
-Infix "\R/" := relation_disjunction (at level 85, right associativity) : relation_scope.
+(* Infix "<R>" := relation_equivalence (at level 95, no associativity) : relation_scope. *)
+(* Infix "-R>" := subrelation (at level 70) : relation_scope. *)
+(* Infix "/R\" := relation_conjunction (at level 80, right associativity) : relation_scope. *)
+(* Infix "\R/" := relation_disjunction (at level 85, right associativity) : relation_scope. *)
 
-Open Local Scope relation_scope.
+(* Open Local Scope relation_scope. *)
 
 (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
 
@@ -258,7 +256,7 @@ Program Instance subrelation_preorder :
    on the carrier. *)
 
 Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
-  partial_order_equivalence : relation_equivalence eqA (R /R\ flip R).
+  partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip R)).
 
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism 
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index dd8536d572..a518faa570 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -15,7 +15,7 @@
 
 (** Unicode lambda abstraction, does not work with factorization of lambdas. *)
 
-Notation  " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope.
+Notation  " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T at level 10, y at next level, no associativity) : program_scope.
 
 (** Notations for the unit type and value. *)
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index f2dcdd0e07..c8c0c8b169 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -96,33 +96,25 @@ Ltac subst_no_fail :=
 
 Tactic Notation "subst" "*" := subst_no_fail.
 
+Ltac on_application f tac T :=
+  match T with
+    | context [f ?x ?y ?z ?w ?v ?u ?a ?b ?c] => tac (f x y z w v u a b c)
+    | context [f ?x ?y ?z ?w ?v ?u ?a ?b] => tac (f x y z w v u a b)
+    | context [f ?x ?y ?z ?w ?v ?u ?a] => tac (f x y z w v u a)
+    | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u)
+    | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v)
+    | context [f ?x ?y ?z ?w] => tac (f x y z w)
+    | context [f ?x ?y ?z] => tac (f x y z)
+    | context [f ?x ?y] => tac (f x y) 
+    | context [f ?x] => tac (f x)
+  end.
+  
 (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *)
+
 Ltac on_call f tac :=
   match goal with
-    | H : ?T |- _  =>
-      match T with
-        | context [f ?x ?y ?z ?w ?v ?u ?a ?b ?c] => tac (f x y z w v u a b c)
-        | context [f ?x ?y ?z ?w ?v ?u ?a ?b] => tac (f x y z w v u a b)
-        | context [f ?x ?y ?z ?w ?v ?u ?a] => tac (f x y z w v u a)
-        | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u)
-        | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v)
-        | context [f ?x ?y ?z ?w] => tac (f x y z w)
-        | context [f ?x ?y ?z] => tac (f x y z)
-        | context [f ?x ?y] => tac (f x y) 
-        | context [f ?x] => tac (f x)
-      end
-    | |- ?T  =>
-      match T with
-        | context [f ?x ?y ?z ?w ?v ?u ?a ?b ?c] => tac (f x y z w v u a b c)
-        | context [f ?x ?y ?z ?w ?v ?u ?a ?b] => tac (f x y z w v u a b)
-        | context [f ?x ?y ?z ?w ?v ?u ?a] => tac (f x y z w v u a)
-        | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u)
-        | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v)
-        | context [f ?x ?y ?z ?w] => tac (f x y z w)
-        | context [f ?x ?y ?z] => tac (f x y z)
-        | context [f ?x ?y] => tac (f x y)
-        | context [f ?x] => tac (f x)
-      end
+    | |- ?T  => on_application f tac T
+    | H : ?T |- _  => on_application f tac T
   end.
 
 (* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object. *)
@@ -130,14 +122,35 @@ Ltac on_call f tac :=
 Ltac destruct_call f :=
   let tac t := destruct t in on_call f tac.
 
+Ltac destruct_calls f := repeat destruct_call f.
+
+Ltac destruct_call_in f H :=
+  let tac t := destruct t in
+  let T := type of H in
+    on_application f tac T.
+
 Ltac destruct_call_as f l :=
   let tac t := destruct t as l in on_call f tac.
 
+Ltac destruct_call_as_in f l H :=
+  let tac t := destruct t as l in
+  let T := type of H in
+    on_application f tac T.
+
 Tactic Notation "destruct_call" constr(f) := destruct_call f.
 
 (** Permit to name the results of destructing the call to [f]. *)
 
-Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l.
+Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := 
+  destruct_call_as f l.
+
+(** Specify the hypothesis in which the call occurs as well. *)
+
+Tactic Notation "destruct_call" constr(f) "in" hyp(id) := 
+  destruct_call_in f id.
+
+Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(id) := 
+  destruct_call_as_in f l id.
 
 (** Try to inject any potential constructor equality hypothesis. *)