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

4 files changed, 107 insertions, 37 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index f56089b1e5..a1d978b1f9 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 3124e10a0f..f768e98e47 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 f5813e40b3..9369b067fc 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 567ed7500d..db67d14731 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
+