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

1 files changed, 38 insertions, 25 deletions

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index f2dcdd0e0..c8c0c8b16 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. *)