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

2 files changed, 39 insertions, 26 deletions

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. *)