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

7 files changed, 186 insertions, 55 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 28c2acb81..b6a3c985a 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -166,15 +166,15 @@ GEXTEND Gram
     [ [ c = global -> AN c
       | s = ne_string -> ByNotation (loc,s) ] ]
   ;
-  occurrences:
+  occs:
     [ [ "at"; nl = LIST1 int_or_var -> nl
       | -> [] ] ]
   ;
   pattern_occ:
-    [ [ c = constr; nl = occurrences -> (nl,c) ] ]
+    [ [ c = constr; nl = occs -> (nl,c) ] ]
   ;
   unfold_occ:
-    [ [ c = smart_global; nl = occurrences -> (nl,c) ] ]
+    [ [ c = smart_global; nl = occs -> (nl,c) ] ]
   ;
   intropatterns:
     [ [ l = LIST0 simple_intropattern -> l ]]
@@ -266,10 +266,10 @@ GEXTEND Gram
     ] ]
   ;
   hypident_occ:
-    [ [ (id,l)=hypident; occs=occurrences -> ((occs,id),l) ] ]
+    [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ]
   ;
   clause:
-    [ [ "in"; "*"; occs=occurrences ->
+    [ [ "in"; "*"; occs=occs ->
           {onhyps=None; onconcl=true; concl_occs=occs}
       | "in"; "*"; "|-"; (b,occs)=concl_occ ->
           {onhyps=None; onconcl=b; concl_occs=occs}
@@ -277,13 +277,13 @@ GEXTEND Gram
           {onhyps=Some hl; onconcl=b; concl_occs=occs}
       | "in"; hl=LIST0 hypident_occ SEP"," ->
           {onhyps=Some hl; onconcl=false; concl_occs=[]}
-      | occs=occurrences ->
+      | occs=occs ->
 	  {onhyps=Some[]; onconcl=true; concl_occs=occs}
       | ->
 	  {onhyps=Some[]; onconcl=true; concl_occs=[]} ] ]
   ;
   concl_occ:
-    [ [ "*"; occs = occurrences -> (true,occs)
+    [ [ "*"; occs = occs -> (true,occs)
       | -> (false, []) ] ]
   ;
   simple_clause:
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index f56089b1e..a1d978b1f 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -739,35 +739,41 @@ let refresh_hypinfo env sigma hypinfo =
 let unify_eqn env sigma hypinfo t = 
   try 
     let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
-    let env', c1, c2, car, rel = 
-      match abs with
-	  Some _ -> 
-	    if convertible env cl.evd (if l2r then c1 else c2) t then 
-	      cl, c1, c2, car, rel
-	    else raise Not_found
-	| None ->
-	    let env' =
-	      try clenv_unify allowK ~flags:rewrite_unif_flags
-		CONV (if l2r then c1 else c2) t cl
-	      with Pretype_errors.PretypeError _ ->
-		(* For Ring essentially, only when doing setoid_rewrite *)
-		clenv_unify allowK ~flags:rewrite2_unif_flags
-		  CONV (if l2r then c1 else c2) t cl
-	    in
-	    let env' = 
-	      let mvs = clenv_dependent false env' in
-		clenv_pose_metas_as_evars env' mvs
-	    in
-	    let c1 = Clenv.clenv_nf_meta env' c1 
-	    and c2 = Clenv.clenv_nf_meta env' c2
-	    and car = Clenv.clenv_nf_meta env' car
-	    and rel = Clenv.clenv_nf_meta env' rel in
-	    let ty1 = Typing.mtype_of env'.env env'.evd c1 
-	    and ty2 = Typing.mtype_of env'.env env'.evd c2
-	    in
-	      if convertible env env'.evd ty1 ty2 then
-		env', c1, c2, car, rel
+    let env', c1, c2, car, rel =
+      let left = if l2r then c1 else c2 in
+	match abs with
+	    Some _ -> 
+	      (* Disallow unfolding of a local var. *)
+	      if isVar left || isVar t then
+		if eq_constr left t then
+		  cl, c1, c2, car, rel
+		else raise Not_found
+	      else if convertible env cl.evd left t then
+		cl, c1, c2, car, rel
 	      else raise Not_found
+	  | None ->
+	      let env' =
+		try clenv_unify allowK ~flags:rewrite_unif_flags
+		  CONV left t cl
+		with Pretype_errors.PretypeError _ ->
+		  (* For Ring essentially, only when doing setoid_rewrite *)
+		  clenv_unify allowK ~flags:rewrite2_unif_flags
+		    CONV left t cl
+	      in
+	      let env' = 
+		let mvs = clenv_dependent false env' in
+		  clenv_pose_metas_as_evars env' mvs
+	      in
+	      let c1 = Clenv.clenv_nf_meta env' c1 
+	      and c2 = Clenv.clenv_nf_meta env' c2
+	      and car = Clenv.clenv_nf_meta env' car
+	      and rel = Clenv.clenv_nf_meta env' rel in
+	      let ty1 = Typing.mtype_of env'.env env'.evd c1 
+	      and ty2 = Typing.mtype_of env'.env env'.evd c2
+	      in
+		if convertible env env'.evd ty1 ty2 then
+		  env', c1, c2, car, rel
+		else raise Not_found
     in
     let prf =
       if abs = None then
@@ -1497,12 +1503,12 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
 (*       {cl=cl'; prf=prf; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=None} *)
 
 let get_hyp gl c clause l2r = 
-  match kind_of_term (pf_type_of gl c) with
-      Prod _ -> 
+(*   match kind_of_term (pf_type_of gl c) with *)
+(*       Prod _ ->  *)
 	let hi = decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r in
 	let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
 	  unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl
-    | _ -> decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r
+(*     | _ -> decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r *)
 	
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = false }
 
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 3124e10a0..f768e98e4 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -33,15 +33,68 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 | [ ] -> [ true ]
 END
 
-let pr_occurrences _prc _prlc _prt l =
+let pr_int_list _prc _prlc _prt l =
   let rec aux = function
     | i :: l -> Pp.int i ++ Pp.spc () ++ aux l
     | [] -> Pp.mt()
   in aux l
 
-ARGUMENT EXTEND occurrences TYPED AS int list PRINTED BY pr_occurrences
-| [ integer(i) occurrences(l) ] -> [ i :: l ]
-| [ ] -> [ [] ]
+ARGUMENT EXTEND int_nelist
+  TYPED AS int list 
+  PRINTED BY pr_int_list
+  RAW_TYPED AS int list 
+  RAW_PRINTED BY pr_int_list
+  GLOB_TYPED AS int list
+  GLOB_PRINTED BY pr_int_list
+| [ integer(x) int_nelist(l) ] -> [x::l]
+| [ integer(x) ] -> [ [x] ]
+END
+
+open Rawterm
+
+let pr_occurrences _prc _prlc _prt l =
+  match l with
+    | ArgArg x -> pr_int_list _prc _prlc _prt x
+    | ArgVar (loc, id) -> Nameops.pr_id id
+
+let coerce_to_int = function
+  | VInteger n -> n
+  | v -> raise (CannotCoerceTo "an integer")
+
+let int_list_of_VList = function
+  | VList l -> List.map (fun n -> coerce_to_int n) l
+  | _ -> raise Not_found
+      
+let interp_occs ist gl l = 
+  match l with
+    | ArgArg x -> x
+    | ArgVar (_,id as locid) -> 
+	(try int_list_of_VList (List.assoc id ist.lfun)
+	  with Not_found | CannotCoerceTo _ -> [interp_int ist locid])
+
+let glob_occs ist l = l
+
+let subst_occs evm l = l
+
+type occurrences_or_var = int list or_var
+type occurrences = int list
+
+ARGUMENT EXTEND occurrences
+  TYPED AS occurrences
+  PRINTED BY pr_int_list
+
+  INTERPRETED BY interp_occs
+  GLOBALIZED BY glob_occs
+  SUBSTITUTED BY subst_occs
+
+  RAW_TYPED AS occurrences_or_var
+  RAW_PRINTED BY pr_occurrences
+
+  GLOB_TYPED AS occurrences_or_var
+  GLOB_PRINTED BY pr_occurrences
+
+| [ int_nelist(l) ] -> [ ArgArg l ]
+| [ var(id) ] -> [ ArgVar id ]
 END
 
 (* For Setoid rewrite *)
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index f5813e40b..9369b067f 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -19,9 +19,9 @@ val rawwit_orient : bool raw_abstract_argument_type
 val wit_orient : bool typed_abstract_argument_type
 val orient : bool Pcoq.Gram.Entry.e
 
-val rawwit_occurrences : (int list) raw_abstract_argument_type
+val occurrences : (int list or_var) Pcoq.Gram.Entry.e
+val rawwit_occurrences : (int list or_var) raw_abstract_argument_type
 val wit_occurrences : (int list) typed_abstract_argument_type
-val occurrences : (int list) Pcoq.Gram.Entry.e
 
 val rawwit_morphism_signature :
  Setoid_replace.morphism_signature raw_abstract_argument_type
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 567ed7500..db67d1473 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -152,3 +152,14 @@ val declare_xml_printer :
 
 (* printing *)
 val print_ltac : Libnames.qualid -> std_ppcmds
+
+(* Internals that can be useful for syntax extensions. *)
+
+exception CannotCoerceTo of string
+
+val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> identifier located -> 'a
+
+val interp_int : interp_sign -> identifier located -> int
+
+val error_ltac_variable : loc -> identifier -> Environ.env option -> value -> string -> 'a
+
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.