Work on the "occurrences" tactic argument. It is now possible to pass

lists of occurrences through tactics. Implement the "at" variants of
setoid_replace correspondingly. 
Fix in class_tactics efor w_unify not checking types when unifying a
meta with anything (problematic at top-level only).


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

2 files changed, 72 insertions, 11 deletions

diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 8752f649b..8412cc102 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.SetoidTactics") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -52,33 +52,94 @@ Ltac setoidreplacein H H' t :=
   let Heq := fresh "Heq" in
     cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | t ].
 
+Ltac setoidreplaceinat H H' t occs :=
+  let Heq := fresh "Heq" in
+    cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq in H' at occs ; clear Heq | t ].
+
+Ltac setoidreplaceat H t occs :=
+  let Heq := fresh "Heq" in
+    cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq at occs ; clear Heq | t ].
+
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
   setoidreplace (default_relation x y) idtac.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) :=
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "at" int_or_var_list(o) :=
+  setoidreplaceat (default_relation x y) idtac o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "in" hyp(id) :=
   setoidreplacein (default_relation x y) id idtac.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic(t) :=
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "in" hyp(id) 
+  "at" int_or_var_list(o) :=
+  setoidreplaceinat (default_relation x y) id idtac o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "by" tactic(t) :=
   setoidreplace (default_relation x y) ltac:t.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic(t) :=
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "at" int_or_var_list(o) 
+  "by" tactic(t) :=
+  setoidreplaceat (default_relation x y) ltac:t o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "in" hyp(id) 
+  "by" tactic(t) :=
   setoidreplacein (default_relation x y) id ltac:t.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) :=
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "in" hyp(id) 
+  "at" int_or_var_list(o) 
+  "by" tactic(t) :=
+  setoidreplaceinat (default_relation x y) id ltac:t o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel) :=
   setoidreplace (rel x y) idtac.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "using" "relation" constr(rel) "by" tactic(t) :=
+  "using" "relation" constr(rel)
+  "at" int_or_var_list(o) :=
+  setoidreplaceat (rel x y) idtac o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel) 
+  "by" tactic(t) :=
   setoidreplace (rel x y) ltac:t.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) 
-  "using" "relation" constr(rel) :=
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel) 
+  "at" int_or_var_list(o)  
+  "by" tactic(t) :=
+  setoidreplaceat (rel x y) ltac:t o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel)
+  "in" hyp(id) :=
   setoidreplacein (rel x y) id idtac.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
-  "using" "relation" constr(rel) "by" tactic(t) :=
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel)
+  "in" hyp(id) 
+  "at" int_or_var_list(o) :=
+  setoidreplaceinat (rel x y) id idtac o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel)
+  "in" hyp(id)
+  "by" tactic(t) :=
   setoidreplacein (rel x y) id ltac:t.
 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel) 
+  "in" hyp(id)
+  "at" int_or_var_list(o)  
+  "by" tactic(t) :=
+  setoidreplaceinat (rel x y) id ltac:t o.
+
 (** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back
    to the user to discharge the proof. It essentially amounts to unfold the right amount of [respectful] calls
    and substitute leibniz equalities. One can redefine it using [Ltac add_morphism_tactic ::= t]. *)
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 8f1f26dbc..a5e560c89 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -25,7 +25,7 @@ Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x : A => g (f x).
 
 Hint Unfold compose.
 
-Notation " g ∘ f " := (compose g f)  (at level 50, left associativity) : program_scope.
+Notation " g ∘ f " := (compose g f)  (at level 40, left associativity) : program_scope.
 
 Open Local Scope program_scope.